-- SNAP and SPAN : Towards Dynamic Spatial Ontology, by Pierre Grenon & Barry Smith -- Grenon Smith used first-order logic for their formalization. -- We use CafeOBJ FOPL module. -- Which in turn will be used to construct a behaviour model of a "wayfinding" or GMAPS. -- Working assumption a CafeOBJ module represents an ontology. Ontologies are related using imports and parameterised modules. -- This file contains the high abstract SANP and SPAN ontologies. -- Based on SNAP and SPAN : Towards Dynamic Spatial Ontology, by Pierre Grenon & Barry Smith -- We intend to use CafeOBJ's intra institution relation between equational logic and behavioural logic to handle the trans-ontological relations that cross the SNAP-SPAN divide; -- SNAP is considered as a succession of ontologies -- The principal inter-ontology signatures are: -- e.g.,participant, e.g. ‘the jumper is a participant in the jumping event’ -- e.g., creation, as in ‘burning creates ashes’ -- , for distinct time indices i, j, e .g., change , as in ‘the leg is no longer part of the table’ -- , i = j, e .g., part, as in ‘the leg is part of the table’ (added by PB) -- for SPAN ontologies with different domains or granularities, e.g., as in ‘the poor driving caused an accident’ -- SNAP Spatial Region <-> SPAN Temporal Region -- Projection -- Process PROJECTS onto a temporal axis (SPAN -> SPAN) -- Substance PROJECTS onto a period of time (SNAP -> SPAN) -- Process PROJECTS onto a spatial location (SPAN -> SNAP) -- The following is from General Ontology Baseline, by Scott Farrar and John Bateman -- (SNAP, SPAN), e.g.,participant,a s in ‘the jumper is a participant in the jumping event’ -- (SNAP,SNAP),e .g., part, as in ‘the leg is part of the table’ -- (SPAN,SNAP),e.g., creation, as in ‘burning creates ashes’ -- (SPAN,SPAN),e.g., as in ‘the poor driving caused an accident’ -- The following is from Internet Encylclopedia of Philosophy on Universals, at -- http://www.iep.utm.edu/u/universa.htm -- Universals are a class of mind independent entities, usually contrasted with individuals, -- postulated to ground and explain relations of qualitative identity and resemblance among individuals. -- An apple and a ruby are both red, and their common redness results from sharing a universal. -- Tropes are a type of individual. -- The blue of the sky is a particular trope numerically distinct from the blue trope of your T-shirt, -- even if the two tropes are qualitatively identical. -- There is an inherence relation between a substance and its properties. -- The following noation is from BFO in a Nutshell by Pierre Grenon -- who in turn adapted it from -- The WonderWeb Library of Foundational Ontologies, WonderWeb, C, Borgo, S., Gangemi, A., Guarino, N., Oltramari, A., Schneider, L. (2003) -- ‘PT’, partition -- ‘SB’, subsumption -- ‘DJ’ disjointness -- -- the indexing times do not belong to the SNAP ontologies they index -- Two kinds of intra-ontological relations: -- Relations between SNAP entities which are constituents of the same SNAP ontology. -- Relations which obtain between two SPAN entities which are constituents of the same SNAP ontology. -- Trans-ontological relations exist between SNAP and SPAN entities set include FOPL-CLAUSE on -- Primitive relations common to all ontologies -- Most of these axioms are already built into CafeOBJ module system, where Ontology=Module and Entity=Sort -- So we will not use them mod ONTOLOGY0 { [ Occurrent Continuent < Entity < Ontology ] op entity : Entity -> Bool op OMEGA : Ontology -> Bool op omega : -> Ontology op constituent : Entity Ontology -> Bool -- Everything which exists in the spatio-temporal world is an entity. -- entity(x) stands for: x exists in the spatio-temporal world. -- We can define entity() ax \A[x:Entity] (x :is Entity) -> entity(x) . ax \A[x:Entity] ~(x :is Entity) -> ~(entity(x)) . -- There is no X that is an Entity and an Ontology, they are distinct ax [A1] : \A[o:Ontology] \A[x:Entity] ~(OMEGA(o) & entity(x) & (omega = x)) . -- The only costituents of an ontology are entities and events are constituents of ontologies only ax [A2] : \A[o:Ontology] \A[x:Entity] constituent(x,o) -> (entity(x) & OMEGA(o)) . -- There is not empty ontology i.e there is no ontology of nothing. ax [A3] : \A[o:Ontology] \E[x:Entity] (OMEGA(o)) -> (entity(x) & constituent(x,o)) . -- Conversly, any entity in the domain of our theory is a constituent of some ontology ax [A4] : \A[x:Entity] \E[o:Ontology] entity(x) -> ((OMEGA(o)) & constituent(x,o)) . -- There is at least one ontology, This theorem is provable in CafeOBJ ax [T5] : \E[o:Ontology] (OMEGA(o)) . } -- In order to make our CafeOBJ representaion concsistent with BFO we have two meta-ontological sorts -- At this stage the do not seem of great practical significance. mod ONTOLOGY { pr(EQL) [ Entity < Ontology ] op constituent : Entity Ontology -> Bool -- We refer to material universals by means of terms such as ‘mountain’, ‘lake’, and so on. -- Instantiation(a, u)’ stands for: particular a is an instance of the material universal u’ } mod* MEREOLOGY { pr(ONTOLOGY) op part : Entity Entity -> Bool op part : Entity Entity Ontology -> Bool op properPart : Entity Entity -> Bool op overlap : Entity Entity -> Bool op sum : Entity Entity Entity -> Bool op substance : Entity -> Bool -- op substantial : Entity -> Bool is this different from 'sunstance'? op constituent : Entity Ontology -> Bool -- duplicate included above op P : Entity -> Bool op R : Entity Entity Ontology -> Bool op R : Entity Ontology Entity Ontology -> Bool ax [A5] : \A[x:Entity, y:Entity] part(x, x) . ax [A6] : \A[x:Entity, y:Entity, z:Entity] (part(x, y) & part(y, z)) -> part(x, z) . ax [A7] : \A[x:Entity, y:Entity] (part(x, y) & part(y, x)) -> (x = y) . -- The following are definititions. Should they be CafeOBJ equations (LHS=RHS) rather than axioms (for all x P(x)? ax [A8] : \A[x:Entity, y:Entity] properPart(x:Entity, y:Entity) = (part(x, y) -> ~(x = y)) . ax [A9] : \A[x:Entity, y:Entity] \E[z:Entity] overlap(x, y) = (part(z, x) & part(z, y)) . ax [A10] : \A[x:Entity, y:Entity] \E[z:Entity, z':Entity, w:Entity, w':Entity] sum(z, x, y) = ((overlap(w, x) | overlap(w , y)) <-> overlap(w, z) & ((overlap(w, x) | overlap(w, y)) <-> overlap(w, z')) -> (z == z')) . -- We can use A10 to provide the logic for road and road sections ax [A11] : \A[x:Entity, y:Entity, w:Ontology] \E[z:Entity] (substance(x) & substance(y) & constituent(x, w) & constituent(y, w)) -> (constituent(z, w) & sum(z, x, y)) . -- P is a general predicate, a stand-in for a given predicate, maybe could use view -- P is dissective when all parts of any instances of P also fall under P: ax [D12] : \A[x:Entity, y:Entity] (P(x) & part(y, x)) -> P(y) . -- P is cumulative when the sum of any two instances of P also falls under P: ax [D13] : \A[x:Entity, y:Entity, z:Entity] (sum(z, x, y) & P(x) & P(y)) -> P(z) . -- Some general relations between ontologies. These are not named in paper. ax [R1] : \A[x:Entity, y:Entity, w:Ontology] R(x, y,w ) -> (constituent(x,w ) & constituent(y,w )) . ax [R2] : \A[x:Entity, y:Entity, w:Ontology,w':Ontology] R(x,w,y,w') -> (constituent(x,w ) & constituent(y,w')) . } mod* SNAP { pr(MEREOLOGY) pr(EQL) -- [ Time ] -- from whence? [ SpatialRegion IndependentContinuent DependentContinuent < Continuent < Entity] -- What type of equality? -- Should all variables be of type Bool? ui.e. not sorts -- This would mean we could stay entirely in FOPL e.g. y <-> x instead of y = x ot y == x. -- They we would be saying that y is logically equivalent to x i.e. they have the same logical value. -- Below is a common convention for equality from http://en.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms -- Where equality symbol as a primitive logical symbol. -- The axioms for equality to the axioms for first-order logic are: -- x = x (reflexivity) -- x = y f(...,x,...) = f(...,y,...) for any function f -- x = y -> (P(...,x,...) -> P(...,y,...)) for any relation P (Leibniz's law) -- I will check out FOPL in CafeOBJ for equality. -- op part : Continuent Continuent -> Bool op inheresIn : DependentContinuent SpatialRegion -> Bool -- originally -- op spatialLocation : Continuent SpatialRegion -> Bool -- but move to typeless or sortless op spatialLocation : Entity Entity Ontology -> Bool op spatial-location : Entity Ontology -> Bool op temporalIndex : Ontology Entity -> Bool op SnapOmega : Ontology -> Bool op timeInstant : Entity -> Bool op existsAt : Entity Entity -> Bool op existsDuring : Entity Entity -> Bool op timeRegion : Entity -> Bool op spatialRegion : Entity -> Bool op snapEntity : Entity -> Bool op inheresIn : Entity Entity Ontology -> Bool op substantial : Entity -> Bool -- A SNAP ontology is formed through the depiction of enduring entities existing at a given time (in a given domain at a given level of granularity). -- Such an ontology is analogous to a snapshot, or to the results of a process of sampling. -- Constituents of SNAP ontologies (SnapO) are SNAP entities. -- The predicate SnapEntity is both dissective and cumulative (parts and sums of SNAP entities are SNAP entities themselves). ax [A14] : \A[x:Entity, w:Ontology] (temporalIndex(w,x) & SnapOmega(w)) -> timeInstant(x) . -- Being a constituent of a SNAP ontology amounts to existing (as a continuant) at the time of the ontology’s index. -- ‘ExistsAt(a, t)’ stands for: ‘the SNAP entity a exists at instant t’. -- Here the 't' in temporalIndex(w,t) seems to be time, is it an entity in [A14] ? ax [D15] : \A[x:Entity, t:Entity, w:Ontology] existsAt(x, t) = (SnapOmega(w) & temporalIndex(w,t) & constituent(x, w)) . ax [D16] : \A[x:Entity, y:Entity, z:Entity] existsDuring(x,y) = timeRegion(y) & timeInstant(z) & properPart(z, y) -> existsAt(x, z) . -- There is one distinguished spatial region, namely space or the entire spatial universe (the maximal spatial region). -- All spatial regions are parts of space. SpatialRegion is trivially dissective and cumulative. -- Thus we may define the predicate (with space=y) spatialRegion as follows: ax [D17] : \A[x:Entity, y:Entity] spatialRegion(x) = part(x,y) . -- Spatial regions can serve as locations for SNAP entities. -- Here is a primitive relation of spatial location, symbolized: ‘SpatialLocation’ -- (it corresponds to the notion of exact location in (Casati and Varzi, 1996)). ax [A18] : \A[x:Entity, y:Entity, w:Ontology] (snapEntity(x) & constituent(x, w)) -> spatialLocation(x, y, w ) . ax [A19] : \A[x:Entity, y:Entity, y':Entity, w:Ontology] (spatialLocation(x, y, w) & spatialLocation(x, y', w )) -> (y = y') . -- what type of equality? -- SpatialLocation [A19] is a functional predicate. -- We can denote the spatial location of an entity a in an ontology w via the expression ‘spatial-location(a, w)’. ax [D20] : \A[x:Entity, y:Entity, w:Ontology] spatial-location(x, w) = (y = spatialLocation(x, y, w)) . -- is equality correct -- The endurance and dependence are necessary conditions for SNAP dependent entities, they are not sufficient conditions. -- The distinguishing feature of these entities is that they inhere in substances. -- InheresIn is an intraontological relation between a SNAP dependent entity and its substantial bearer. -- The redness of the ball inheres in the ball; the shape of a landform inheres in the landform. -- Inherence is a form of existential dependence (Husserl, 1913/21; Simons, 1987; Smith, 1997). -- The latter is such that the first of its relata (in the case of inherence, the SNAP dependent entity) exists only in virtue of the existence of the second (the bearer). -- Inherence is also a form of spatial subsumption, i.e., the spatial location of the inhering entity is a part of its bearer’s: ax [A21] : \A[x:Entity, y:Entity, x':Entity, y':Entity, w:Ontology] (inheresIn(x, y, w) & spatialLocation(x, x', w) & spatialLocation(y, y', w )) -> part(x', y', w) . } -- in a CafeOBJ specification the power set of X can be expressed as Set -- For 'pure OO' style specification in CafeOBJ see Alexander Knapp, Natalie Lyabakh, Ulrick Lechner mod* SPAN { pr(ONTOLOGY) pr(EQL) [ SpatioTemporalRegion ProcessualEntity < Occurrent < Entity ] [ TemporalInstant TemporalInterval < ConnectedTemporalRegion ScatteredTemporalRegion < TemporalRegion ] [ ProcessualContext ProcessAggragate Process FiatProcess BoundaryofProcess < ProcessualEntity ] [ SpatioTemporalInstant SpatioTemporalInterval < ConnectedSpatioTemporalRegion ScatteredSpatioTemporalRegion < SpatioTemporalRegion ] op SpanOmega : Ontology -> Bool op timeRegion : Entity -> Bool -- already in SNAP op timeInstant : Entity -> Bool -- already in SNAP op part : Entity Entity -> Bool -- already defined in SNAP op spanEntity : Entity -> Bool op temporalLocation : Entity Entity -> Bool op atTime : Entity Entity -> Bool op temporal-location : Entity -> Bool op cotemporal : Entity Entity -> Bool op temporalPart : Entity Entity -> Bool op temporalSlice : Entity Entity -> Bool op temporalIndex : Ontology Entity -> Bool op processual : Entity -> Bool op event : Entity -> Bool op occursAt : Entity Entity -> Bool op spaceTimeRegion : Entity -> Bool op temporalRestriction : Entity Entity -> Bool op section : Ontology Ontology -> Bool -- SPAN entities are not located in space - -- the assumption that they are so located derived from the fact that each region of space may be put in correspondence with a particular portion of an instantaneous slice of spacetime. -- SPAN ontologies comprehend spatiotemporally extended regions and the occurrents (including changes, as entities in their own right) located at such regions. ax [A22] : \A[w:Ontology] SpanOmega(w) -> (\E[x:Entity] timeRegion(x) & constituent(x, w )) . -- if the quantified is embedded in an expression then brackets. -- Time, the maximal temporal region, is a perdurant, and thus a SPAN entity. -- A temporal region is a part of time. -- TimeRegion may now be defined as follows: ax [D23] : \A[t:Entity] \E[x:Entity] timeRegion(x) = part(x, t) . -- Instants of time are zero-dimensional ax [A24] : \A[x:Entity] spanEntity(x) -> (\E[y:Entity] (timeRegion(y) & temporalLocation(x, y))) . -- The temporal location of each SPAN entity is unique and TemporalLocation is therefore functional: ax [A25] : \A[x:Entity] \A[y:Entity] \A[z:Entity] (temporalLocation(x, y) & temporalLocation(x, z)) -> (z = y) . -- equality -- Instantaneous SPAN entities are located at instants of time. -- We define the intra-ontological relation AtTime: ax [D26] : \A[x:Entity] \A[y:Entity] atTime(x, y) = (temporalLocation(x, y) & timeInstant(y)) . -- Note 'temporal-location(x)' is distinct from 'temporalLocation' ax [D27] : \A[x:Entity] \A[y:Entity] \A[z:Entity] cotemporal(x, y) = (temporal-location(x) = temporal-location(z)) . -- equality ax [D28] : \A[x:Entity] \A[y:Entity] temporalPart(x, y) = part(x, y) & (\A[z:Entity] (part(z, y) & cotemporal(x,z)) -> part(z, x)) . ax [D29] : \A[x:Entity] \A[y:Entity] temporalSlice(x, y) = temporalPart(x, y) & (\E[t:Entity] atTime(x,t)) . -- predicate Event holding of instantaneous processuals: ax [D30] : \A[x:Entity] event(x) = (\E[y:Entity] (processual(y) & temporalSlice(x, y))) . ax [D31] : \A[x:Entity] \A[t:Entity] occursAt(x, t) = (\E[y:Entity] (temporalSlice(y, x) & atTime(y, t)) ) . ax [D32] : \A[x:Entity] \A[spacetime:Entity] spaceTimeRegion(x) = part(x, spacetime) . -- Problem with [D33] "part(temporal-location(x),t))" temporal-location(x) returns Bool not Entity. -- For the moment we will use just part(x,t) -- Also the Es are required on the RHS of definition ax [D33] : \A[w:Ontology] \A[w':Ontology] \E[x:Entity] \E[t:Entity] \E[t':Entity] temporalRestriction(w ,w') = temporalIndex(w, t) & temporalIndex(w',t') & part(t,t') & (constituent(x,w) <-> (constituent(x,w') & part(x,t))) . -- Problem using \E with previously "definition". -- Temp solution put \E on LHS ax [D34] : \A[w:Ontology] \A[w':Ontology] \E[t:Entity] section(w, w') = temporalRestriction(w,w') & temporalIndex(w, t) & timeInstant(t) . -- The uniqueness of temporal location and the putative granularity of ontologies, -- requires that any ontology which has a given SPAN entity as a constituent has its corresponding temporal location as a constituent -- hence, the granularity of processuals is transmitted to the granularity of temporal regions). ax [A35] : \E[x:Entity] \E[y:Entity] \A[w:Ontology] (constituent(x, w ) & temporalLocation(x, y)) -> constituent(y, w ) . } -- All BFO documentation uses FOPL for both SNAP and SPAN axioms and definitions. -- BFO imports ONTOLOGY, SNAP and SPAN and defines the relations between SNAP and SPAN -- Processes cannot exist without their participants, -- At this stage, occurrents are entities that depend on corresponding continuants. -- Relations between Snap and Span entities. -- Rather -- We must establish the different sorts of relationships between SNAP and SPAN entities. -- These fall into three major families: -- dependence (of processes on substances), -- participation (of substances in processes), and -- realization (of roles, functions, plans in processes). -- These are primitive relations. The most fundamental form of participation is between a Snap entity and a temporal slice of a process (an event): -- Participation: PCss(x, y, t) means that x is a substantial which participates in the event y at t. -- Realization: RZss(x, y, t) means that x is in a process of realization in the event y at t. -- Dependence: SDss(x, y, t) means that x is dependent on the event y at t. mod* BFO { -- SNAP and SPAN : Towards Dynamic Spatial Ontology, by Pierre Grenon & Barry Smith say -- Each SNAP ontology is indexed by a single time instant. -- Each SPAN ontology by a single time interval. -- Do we need time paramterized SNAP and SPAN module? pr(SNAP) pr(SPAN) -- These 3 inter-ontology relations are from WonderWeb Deliverable D18 Ontology Library, by Masolo, Borgo, Gangemi, Guarino,Oltramari (349 pages!) op participation : SpatialRegion ProcessualEntity TemporalInstant -> Bool op realization : SpatialRegion ProcessualEntity TemporalInstant -> Bool op dependence : SpatialRegion ProcessualEntity TemporalInstant -> Bool op participatesIn : Entity Ontology Entity Ontology -> Bool op existsDuring : Entity Entity -> Bool op overlap : Entity Entity Ontology -> Bool -- SNAP relations indexed by time -- op temporalLocation : Continuent TemporalRegion -> Bool op temporalLocation : Entity Entity Ontology -> Bool -- already in SPAN -- in SNAP -- op existsAt : Continuent TemporalInstant -> Bool op existsDuring : Entity Entity -> Bool op surface : Entity Ontology -> Bool -- There is a family of other trans-ontological relations between SNAP and SPAN entities, of which not only -- participation but also -- initiation, -- termination, -- creation, -- destruction, -- sustenance, -- deterioration, -- facilitation, -- hindrance (for details, see Grenon, 2003; Smith and Grenon, 2003). -- Here, we describe the basic intuitions of the framework, taking as prototypical the example of participation. -- A participant in a process exists during a time which overlaps the temporal location of the process. -- Original paper says "(substantial(x) & processual(y))" I have temporalily changed it to "(substantial(x) & processual(y))", will check ax [A36] : \A[w:Ontology] \A[w':Ontology] \A[a:Entity] \A[b:Entity] participatesIn(a, w, b, w') -> (substantial(a) & processual(b)) . -- The following [A37] ia a SNAP-SPAN Trans-ontology -- Could not find enough in main paper, the following is from IFOMIS REPORTS ISSN 1611-4019, (IFOMIS) 06/2003 (aka BFO in a Nutshell) byPierre Grenon -- TemporalLocation(x,y) means that x is the temporal region at which y is (uniquely) located. (It is exact temporal location.) -- It seems that the ontology parameter was added below. -- BFO ought to be given an interval calculus a la Allen on extended regions. -- In addition, generalized temporal order on non regions will be definable straightforwardly from order relations on regions and locational relations. ax [A37] : \A[w:Ontology]\A[w':Ontology] \A[a:Entity]\A[b:Entity]\A[t:Entity]\A[s:Entity]\A[y:Entity]\A[x:Entity] participatesIn(a, w, b, w') & existsDuring(x,t) & temporalLocation(y,s,w) -> overlap(t, s, w') . -- SNAP and SPAN relations indexed by time. -- op temporalIndex : Ontology TemporalRegion -> Bool -- An ontology can only have one time index, This is a meta-level axiom, yet seems to rely on SPAN? } mod* GEODYNAMIC { pr(BFO) op surfaceGeoSpatialRegion : Entity Ontology -> Bool -- op geoTimeRegion : Entity -> Bool op timeSlice : Entity Entity -> Bool op life : Entity -> Entity op geoSpacetimeRegion : Entity -> Bool op SnapGeoEntity : Entity -> Bool op SpanGeoEntity : Entity -> Bool op spatiotemporalLocation : Entity Entity -> Bool op geoSpatialRegion : Entity -> Bool op geoTimeRegion : Entity -> Bool op existsAt : Entity Entity Ontology -> Bool op attributedTo : Entity Entity Ontology -> Bool -- Geospatial regions are regions of space at or in which are located parts of the Earth or of the Earth’s atmosphere at or near its surface -- The entity surface(earth) is a SNAP substantial entity existentially dependent upon earth, and it has a specific spatial location at any given time. -- We may now define surface geospatial regions as spatial locations of parts of the surface of the Earth: -- The predicate cannot be used surface(earth, w) will fix later -- Also the \E cannot be used on RHS of definition fix later ax [D38] : \A[w:Ontology]\A[w':Ontology]\A[x:Entity]\A[earth:Entity] surfaceGeoSpatialRegion(x, w) = (\E[y:Entity] spatialRegion(x) & part(y, y) -> spatialLocation(y, x, w )) . -- The entity surface(earth) is a SNAP substantial entity existentially dependent upon earth, and it has a specific spatial location at any given time. -- Geotemporal Regions are the regions of time during which the Earth exists: ax [D39] : \A[w:Ontology]\A[w':Ontology]\A[x:Entity]\E[y:Entity]\A[earth:Entity] geoTimeRegion(x) = (timeRegion(x) & timeSlice(y, x)) -> existsAt(earth, y) . -- Since the Earth is a SNAP entity, it has a life, which is a SPAN entity. -- The Earth exists at any time at which the process we call its life is occurring, and conversely: -- We cannot use life(earth) must fix ax [T40] : \A[t:Entity]\A[earth:Entity] existsAt(earth, t) <-> occursAt(life(earth), t) . -- The geotemporal regions are precisely the parts of the region of time occupied by the life of the Earth: ax [T41] : \A[x:Entity]\A[y:Entity]\A[earth:Entity] geoTimeRegion(x) <-> (temporalLocation(life(earth),y) & part(x, y)) . -- Geospatiotemporal Regions are the regions of spacetime which are parts of the spatiotemporal location of the life of the Earth: ax [D42] : \A[x:Entity]\A[y:Entity]\A[earth:Entity] geoSpacetimeRegion(x) = spatiotemporalLocation(life(earth), y) & part(x, y) . ax [A43] : \A[w:Ontology]\A[x:Entity]\E[y:Entity] SnapGeoEntity(x) & constituent(x, w) -> geoSpatialRegion(y) & spatialLocation(x, y, w) . ax [A44] : \A[w:Ontology]\A[x:Entity] SnapGeoEntity(x) & constituent(x, w) -> (\E[y:Entity]\E[w':Ontology] SpanOmega(w') & constituent(x, w') & geoTimeRegion(y) & existsAt(x, y, w )) . -- existsAt has 3 args ax [A45] : \A[w:Ontology]\A[x:Entity] SpanGeoEntity(x) & constituent(x, w) -> (\E[y:Entity]\E[w':Ontology] constituent(x, w') & geoSpacetimeRegion(y) & spatiotemporalLocation(x, y)) . -- For instance, there is a portion of the elevation field of the Earth corresponding to Mont Blanc. ax [A46] : \A[w:Ontology]\A[x:Entity]\A[y:Entity]\A[t:Entity]\A[z:Entity] attributedTo(x, y, w) & temporalIndex(w, t) -> (\A[x':Entity]\E[y':Entity]\E[w':Ontology] SpanOmega(w') & temporalIndex(w', t) & inheresIn(x, z, w')) . -- There has to be additional constraints on attribution, e.g., we may only allocate an attribute which depends on a field at a region which is part of that of the field. ax [A47] : \A[w:Ontology]\A[x:Entity]\A[x':Entity]\A[y:Entity]\A[y':Entity] attributedTo(x, y, w) & spatialLocation(x, x', w) & spatialLocation(y, y', w ) -> part(x', y', w) . } eof open ONTOLOGY . -- proof if there is an entity then there is at least one ontology ax entity(x:Entity) . goal \E[o:Ontology] (OMEGA(o)) . . option reset . flag(auto, on) . flag(very-verbose,on) . param(max-proofs, 1) . resolve . close eof -- In order to be used in a manageable SNAP way in temporal contexts requires a temporal logic of a certain grade. -- Time should be in SPAN, but just for the moment. mod! TIME { pr(ONTOLOGY) [ TimeInstant < TimeRegion < Time ] op timeRegion : Time -> Bool op temporalIndex : Ontology Time -> Bool ax \A[t:TimeRegion] (t :is TimeRegion) -> timeRegion(t) . ax \A[t:TimeRegion] ~(t :is TimeRegion) -> ~(timeRegion(t)) . ax \A[a:Ontology, t:TimeRegion] temporalIndex(a,t) -> (OMEGA(a) & timeRegion(t)) . } mod* SNAPMOD{ [ Ontology < Thing < SNAP SPAN ] -- Represents spatial ontology op OMEGA : Ontology -> Bool op omega -> Ontology -- Everything which exists in the spatio-temporal world is an entity. -- Entity(x) stands for: x exists in the spatio-temporal world. op Entity : Thing -> Bool var x : Ontology ceq Entity(x) = true if x :is Thing . eq [A1] : (OMEGA(omega)) && (Entity(x)) && (omega <-> x) = true . -- A1 } mod* SPAN{ -- represents spatial ontology } -- A Fascinating Country in the World of Computing By Larry Wos, Gail W. Pieper -- Parts and Places By Roberto Casati, Achille C. Varzi -- Four-Dimensionalism: An Ontology of Persistence and Time By Theodore Sider -- "Algebraic Specifications of a Knowledge Based Approach for. Cognitive Mapping in a Street Network" [snap] Classes continuant dependent_continuant disposition fiat_object_part function independent_continuant line object object_aggregate object_boundary point quality realizable_entity role site spatial_region surface volume [snap] Classes End [span] Classes connected_spatiotemporal_region connected_temporal_region fiat_process_part occurrent process process_boundary processual_context processual_entity scattered_spatiotemporal_region scattered_temporal_region spatiotemporal_instant spatiotemporal_interval spatiotemporal_region temporal_instant temporal_interval temporal_region [span] Classes