diff --git a/documentation/temporal extensions/temporalized relations/temporalized-relations.pdf b/documentation/temporal extensions/temporalized relations/temporalized-relations.pdf new file mode 100644 index 0000000..4a3118f Binary files /dev/null and b/documentation/temporal extensions/temporalized relations/temporalized-relations.pdf differ diff --git a/src/common logic/release-notes-2024-01-10.txt b/src/common logic/release-notes-2024-01-10.txt new file mode 100644 index 0000000..ffe0515 --- /dev/null +++ b/src/common logic/release-notes-2024-01-10.txt @@ -0,0 +1,254 @@ +Axioms whose logical form changed: +---------------------------------- + +Axiom has-last-instant-domain-range has changed [jtk-1]->[jtk-2] + +(:forall (?a ?b) (:forall (?a ?b) + (:implies (has-last-instant ?a ?b) (:implies (has-last-instant ?a ?b) + (:and (:exists (?t) (instance-of ?a temporal-region ?t)) | (:and (instance-of ?a temporal-region ?a) + (:exists (?t) (instance-of ?b temporal-instant ?t))))) | (instance-of ?b temporal-instant ?b)))) + + +Axiom definition-of-temporal-part-for-temporal-regions has changed [cmy-1]->[cmy-2] + +(:forall (?b ?c) (:forall (?b ?c) + (:implies (:implies + (:and (:exists (?t) (instance-of ?b temporal-region ?t)) | (:and (instance-of ?b temporal-region ?b) + (:exists (?t) (instance-of ?c temporal-region ?t))) | (instance-of ?c temporal-region ?c)) + (:iff (temporal-part-of ?b ?c) (occurrent-part-of ?b ?c)))) (:iff (temporal-part-of ?b ?c) (occurrent-part-of ?b ?c)))) + + +Axiom has-temporal-part.one-dimensional-temporal-region->or-one-dimensional-temporal-region-zero-dimensional-temporal-region has changed [eeg-1]->[eeg-2] + +(:forall (?p ?q) (:forall (?p ?q) + (:implies (has-temporal-part ?p ?q) (:implies (has-temporal-part ?p ?q) + (:implies | (:implies (instance-of ?p one-dimensional-temporal-region ?p) + (:exists (?t) (instance-of ?p one-dimensional-temporal-region ?t)) | (:or (instance-of ?q one-dimensional-temporal-region ?q) + (:exists (?t) / (instance-of ?q zero-dimensional-temporal-region ?q))))) + (:or (instance-of ?q one-dimensional-temporal-region ?t) < + (instance-of ?q zero-dimensional-temporal-region ?t)))))) < + + +Axiom occupies-temporal-region-domain-range has changed [lyx-1]->[lyx-2] + +(:forall (?a ?b) (:forall (?a ?b) + (:implies (occupies-temporal-region ?a ?b) (:implies (occupies-temporal-region ?a ?b) + (:and (:and + (:exists (?t) (:exists (?t) + (:or (instance-of ?a process ?t) (:or (instance-of ?a process ?t) + (instance-of ?a process-boundary ?t))) (instance-of ?a process-boundary ?t))) + (:exists (?t) (instance-of ?b temporal-region ?t))))) | (instance-of ?b temporal-region ?b)))) + + +Axiom temporal-part-of.one-dimensional-temporal-region->one-dimensional-temporal-region has changed [mei-1]->[mei-2] + +(:forall (?p ?q) (:forall (?p ?q) + (:implies (temporal-part-of ?p ?q) (:implies (temporal-part-of ?p ?q) + (:implies | (:implies (instance-of ?p one-dimensional-temporal-region ?p) + (:exists (?t) (instance-of ?p one-dimensional-temporal-region ?t)) / (instance-of ?q one-dimensional-temporal-region ?q)))) + (:exists (?t) < + (instance-of ?q one-dimensional-temporal-region ?t))))) < + + +Axiom has-first-instant-domain-range has changed [fwk-1]->[fwk-2] + +(:forall (?a ?b) (:forall (?a ?b) + (:implies (has-first-instant ?a ?b) (:implies (has-first-instant ?a ?b) + (:and (:exists (?t) (instance-of ?a temporal-region ?t)) | (:and (instance-of ?a temporal-region ?a) + (:exists (?t) (instance-of ?b temporal-instant ?t))))) | (instance-of ?b temporal-instant ?b)))) + + +Axiom temporal-part-of.temporal-region<->temporal-region has changed [mjn-1]->[mjn-2] + +(:forall (?p ?q) (:forall (?p ?q) + (:implies (temporal-part-of ?p ?q) (:implies (temporal-part-of ?p ?q) + (:iff (:exists (?t) (instance-of ?p temporal-region ?t)) | (:iff (instance-of ?p temporal-region ?p) + (:exists (?t) (instance-of ?q temporal-region ?t))))) | (instance-of ?q temporal-region ?q)))) + + +Axiom has-temporal-part.zero-dimensional-temporal-region->zero-dimensional-temporal-region has changed [bnt-1]->[bnt-2] + +(:forall (?p ?q) (:forall (?p ?q) + (:implies (has-temporal-part ?p ?q) (:implies (has-temporal-part ?p ?q) + (:implies | (:implies (instance-of ?p zero-dimensional-temporal-region ?p) + (:exists (?t) / (instance-of ?q zero-dimensional-temporal-region ?q)))) + (instance-of ?p zero-dimensional-temporal-region ?t)) < + (:exists (?t) < + (instance-of ?q zero-dimensional-temporal-region ?t))))) < + + +Axiom temporally-projects-onto-domain-range has changed [cvr-1]->[cvr-2] + +(:forall (?a ?b) (:forall (?a ?b) + (:implies (temporally-projects-onto ?a ?b) (:implies (temporally-projects-onto ?a ?b) + (:and (:exists (?t) (instance-of ?a spatiotemporal-region ?t)) (:and (:exists (?t) (instance-of ?a spatiotemporal-region ?t)) + (:exists (?t) (instance-of ?b temporal-region ?t))))) | (instance-of ?b temporal-region ?b)))) + + +Axiom occurrent-part-of.temporal-region<->temporal-region has changed [gjl-1]->[gjl-2] + +(:forall (?p ?q) (:forall (?p ?q) + (:implies (occurrent-part-of ?p ?q) (:implies (occurrent-part-of ?p ?q) + (:iff (:exists (?t) (instance-of ?p temporal-region ?t)) | (:iff (instance-of ?p temporal-region ?p) + (:exists (?t) (instance-of ?q temporal-region ?t))))) | (instance-of ?q temporal-region ?q)))) + + +Axiom temporal-part-of-is-reflexive-on-temporal-region has changed [dbj-1]->[dbj-2] + +(:forall (?a) (:forall (?a) + (:implies (:exists (?t) (instance-of ?a temporal-region ?t)) | (:implies (instance-of ?a temporal-region ?a) + (temporal-part-of ?a ?a))) (temporal-part-of ?a ?a))) + + +Axiom temporal-instant-only-has-self-as-part has changed [pir-1]->[pir-2] + +(:forall (?p ?q) (:forall (?p ?q) + (:implies (:implies + (:and (:exists (?t) (instance-of ?p temporal-instant ?t)) | (:and (instance-of ?p temporal-instant ?p) + (has-temporal-part ?p ?q)) (has-temporal-part ?p ?q)) + (:= ?p ?q))) (:= ?p ?q))) + + +Axiom every-temporal-region-is-projection-from-spatiotemporal-region has changed [xco-1]->[xco-2] + +(:forall (?tr) (:forall (?tr) + (:implies (:exists (?t) (instance-of ?tr temporal-region ?t)) | (:implies (instance-of ?tr temporal-region ?tr) + (:exists (?st) (:exists (?st) + (:and (:exists (?t) (instance-of ?st spatiotemporal-region ?t)) (:and (:exists (?t) (instance-of ?st spatiotemporal-region ?t)) + (temporally-projects-onto ?st ?tr))))) (temporally-projects-onto ?st ?tr))))) + + +Axiom temporal-regions-instance-of-at-self has changed [tvx-1]->[tvx-2] + +(:forall (?a ?u) (:forall (?a ?u) + (:implies | (:iff + (:exists (?t) (:exists (?t) + (:and (instance-of ?a temporal-region ?t) (instance-of ?a ?u ?t))) (:and (instance-of ?a temporal-region ?t) (instance-of ?a ?u ?t))) + (instance-of ?a ?u ?a))) (instance-of ?a ?u ?a))) + + +Axioms whose name changed: +-------------------------- + + +Axioms whose descriptions only changed: +--------------------------------------- + +Axiom description for s-depends-means-bearer-exists-when-dependent-exists [iyu-1] has changed, +was: 'If x s-depends-on y then there's at least one time when they both exist' +now: 'If s s-depends-on c then there's at least one time when they both exist and whenever s exists, c must also exist' + + +Only in old theory: +------------------- + +Axiom inheres-in-domain-range [lmq-1]: +inheres-in has domain specifically-dependent-continuant and range independent-continuant but not spatial-region +(:forall (?a ?b) + (:implies (inheres-in ?a ?b) + (:and + (:exists (?t) + (instance-of ?a specifically-dependent-continuant ?t)) + (:exists (?t) + (:and (instance-of ?b independent-continuant ?t) + (:not (instance-of ?b spatial-region ?t))))))) + + +Only in new theory: +------------------- + +Axiom occupying-a-three-dimensional-spatial-region-is-rigid [rlf-1]: +The dimensionality of the region of something occupying a three dimensional spatial region does not change +(:forall (?m ?s) + (:implies + (:exists (?t) + (:and (occupies-spatial-region ?m ?s ?t) + (instance-of ?s three-dimensional-spatial-region ?t))) + (:forall (?t1 ?s1) + (:implies (occupies-spatial-region ?m ?s1 ?t1) + (instance-of ?s1 three-dimensional-spatial-region ?t1))))) + +Axiom fiat-line-occupies-1d-spatial-regions [kcq-1]: +A fiat line occupies a one-dimensional spatial region +(:forall (?x ?t) + (:implies (instance-of ?x fiat-line ?t) + (:exists (?s ?tp) + (:and (temporal-part-of ?tp ?t) + (occupies-spatial-region ?x ?s ?tp) + (instance-of ?s one-dimensional-spatial-region ?tp))))) + +Axiom occupying-a-one-dimensional-spatial-region-is-rigid [qfe-1]: +The dimensionality of the region of something occupying a one dimensional spatial region does not change +(:forall (?m ?s) + (:implies + (:exists (?t) + (:and (occupies-spatial-region ?m ?s ?t) + (instance-of ?s one-dimensional-spatial-region ?t))) + (:forall (?t1 ?s1) + (:implies (occupies-spatial-region ?m ?s1 ?t1) + (instance-of ?s1 one-dimensional-spatial-region ?t1))))) + +Axiom occupying-a-two-dimensional-spatial-region-is-rigid [dor-1]: +The dimensionality of the region of something occupying a two dimensional spatial region does not change +(:forall (?m ?s) + (:implies + (:exists (?t) + (:and (occupies-spatial-region ?m ?s ?t) + (instance-of ?s two-dimensional-spatial-region ?t))) + (:forall (?t1 ?s1) + (:implies (occupies-spatial-region ?m ?s1 ?t1) + (instance-of ?s1 two-dimensional-spatial-region ?t1))))) + +Axiom all-participation-at-process-occupied-temporal-region [kxe-1]: +If c participates in p at t and p occupies-temporal-region r then t is part of r +(:forall (?c ?p ?r ?t) + (:implies + (:and (occupies-temporal-region ?p ?r) (participates-in ?c ?p ?t)) + (temporal-part-of ?t ?r))) + +Axiom fiat-surface-occupies-2d-spatial-regions [fpl-1]: +A fiat surface occupies a two-dimensional spatial region +(:forall (?x ?t) + (:implies (instance-of ?x fiat-surface ?t) + (:exists (?s ?tp) + (:and (temporal-part-of ?tp ?t) + (occupies-spatial-region ?x ?s ?tp) + (instance-of ?s two-dimensional-spatial-region ?tp))))) + +Axiom all-role-types-are-rigid [bks-1]: +No role changes type during its existence +(:forall (?o) + (:implies (:exists (?t) (instance-of ?o role ?t)) + (:forall (?u) + (:implies (:exists (?t) (instance-of ?o ?u ?t)) + (:forall (?t) + (:iff (instance-of ?o role ?t) (instance-of ?o ?u ?t))))))) + +Axiom occupying-a-zero-dimensional-spatial-region-is-rigid [fok-1]: +The dimensionality of the region of something occupying a zero dimensional spatial region does not change +(:forall (?m ?s) + (:implies + (:exists (?t) + (:and (occupies-spatial-region ?m ?s ?t) + (instance-of ?s zero-dimensional-spatial-region ?t))) + (:forall (?t1 ?s1) + (:implies (occupies-spatial-region ?m ?s1 ?t1) + (instance-of ?s1 zero-dimensional-spatial-region ?t1))))) + +Axiom occupies-spatial-region.material-entity->three-dimensional-spatial-region [ocw-1]: +If a occupies-spatial-region b then if a is an instance of material-entity then b is an instance of three-dimensional-spatial-region +(:forall (?p ?q ?t) + (:implies + (:and (occupies-spatial-region ?p ?q ?t) + (instance-of ?p material-entity ?t)) + (instance-of ?q three-dimensional-spatial-region ?t))) + +Axiom fiat-point-occupies-0d-spatial-regions [alm-1]: +A fiat point occupies a zero-dimensional spatial region +(:forall (?x ?t) + (:implies (instance-of ?x fiat-point ?t) + (:exists (?tp ?s) + (:and (temporal-part-of ?tp ?t) + (occupies-spatial-region ?x ?s ?tp) + (instance-of ?s zero-dimensional-spatial-region ?tp))))) + diff --git a/src/owl/temporal extensions/temporalized relations/common logic/temporalized-relations.cl b/src/owl/temporal extensions/temporalized relations/common logic/temporalized-relations.cl new file mode 100644 index 0000000..d6996c4 --- /dev/null +++ b/src/owl/temporal extensions/temporalized relations/common logic/temporalized-relations.cl @@ -0,0 +1,288 @@ +(cl:comment ' +BFO 2020 Axiomatization, generated 2024/01/08 +The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020 +Author: Alan Ruttenberg - alanruttenberg(at)gmail.com +This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/' + + (cl:text + + (cl:ttl https://basic-formal-ontology.org/2020/formulas/clif/temporalized-relations.cl + + (cl:outdiscourse has-proper-continuant-part-at-all-times proper-continuant-part-of-at-all-times spatially-projects-onto-at-all-times occupies-spatial-region-at-all-times generically-depends-on-at-all-times has-continuant-part-at-all-times has-material-basis-at-all-times continuant-part-of-at-all-times material-basis-of-at-all-times is-concretized-by-at-all-times participates-in-at-all-times has-participant-at-all-times has-member-part-at-all-times member-part-of-at-all-times is-carrier-of-at-all-times location-of-at-all-times concretizes-at-all-times located-in-at-all-times has-proper-continuant-part has-proper-continuant-part-at-some-time proper-continuant-part-of proper-continuant-part-of-at-some-time spatially-projects-onto spatially-projects-onto-at-some-time occupies-spatial-region occupies-spatial-region-at-some-time generically-depends-on generically-depends-on-at-some-time has-continuant-part has-continuant-part-at-some-time has-material-basis has-material-basis-at-some-time continuant-part-of continuant-part-of-at-some-time material-basis-of material-basis-of-at-some-time is-concretized-by is-concretized-by-at-some-time instance-of rdf-type participates-in participates-in-at-some-time has-participant has-participant-at-some-time has-member-part has-member-part-at-some-time member-part-of member-part-of-at-some-time is-carrier-of is-carrier-of-at-some-time location-of location-of-at-some-time concretizes concretizes-at-some-time located-in exists-at located-in-at-some-time) + + (cl:comment "located-in at some time [asd-1]" + (forall (p q) + (iff (located-in-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (located-in p q t)))))) + + + (cl:comment "concretizes at some time [gkc-1]" + (forall (p q) + (iff (concretizes-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (concretizes p q t)))))) + + + (cl:comment "location-of at some time [spm-1]" + (forall (p q) + (iff (location-of-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (location-of p q t)))))) + + + (cl:comment "is-carrier-of at some time [qkm-1]" + (forall (p q) + (iff (is-carrier-of-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (is-carrier-of p q t)))))) + + + (cl:comment "member-part-of at some time [kax-1]" + (forall (p q) + (iff (member-part-of-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (member-part-of p q t)))))) + + + (cl:comment "has-member-part at some time [smy-1]" + (forall (p q) + (iff (has-member-part-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (has-member-part p q t)))))) + + + (cl:comment "has-participant at some time [ebs-1]" + (forall (p q) + (iff (has-participant-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (has-participant p q t)))))) + + + (cl:comment "participates-in at some time [oia-1]" + (forall (p q) + (iff (participates-in-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (participates-in p q t)))))) + + + (cl:comment "rdf:type is interpreted as meaning an instance is a given type whenever it exists, and that the instance exists at some point. [fyy-1]" + (forall (c i) + (iff (rdf-type c i) + (and (forall (t) (if (exists-at i t) (instance-of i c t))) + (exists (t) (exists-at i t)))))) + + + (cl:comment "is-concretized-by at some time [zgk-1]" + (forall (p q) + (iff (is-concretized-by-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (is-concretized-by p q t)))))) + + + (cl:comment "material-basis-of at some time [exa-1]" + (forall (p q) + (iff (material-basis-of-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (material-basis-of p q t)))))) + + + (cl:comment "continuant-part-of at some time [lzq-1]" + (forall (p q) + (iff (continuant-part-of-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (continuant-part-of p q t)))))) + + + (cl:comment "has-material-basis at some time [fqc-1]" + (forall (p q) + (iff (has-material-basis-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) (has-material-basis p q t)))))) + + + (cl:comment "has-continuant-part at some time [jvz-1]" + (forall (p q) + (iff (has-continuant-part-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) + (has-continuant-part p q t)))))) + + + (cl:comment "generically-depends-on at some time [vrq-1]" + (forall (p q) + (iff (generically-depends-on-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) + (generically-depends-on p q t)))))) + + + (cl:comment "occupies-spatial-region at some time [yci-1]" + (forall (p q) + (iff (occupies-spatial-region-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) + (occupies-spatial-region p q t)))))) + + + (cl:comment "spatially-projects-onto at some time [epa-1]" + (forall (p q) + (iff (spatially-projects-onto-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) + (spatially-projects-onto p q t)))))) + + + (cl:comment "proper-continuant-part-of at some time [sql-1]" + (forall (p q) + (iff (proper-continuant-part-of-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) + (proper-continuant-part-of p q t)))))) + + + (cl:comment "has-proper-continuant-part at some time [ule-1]" + (forall (p q) + (iff (has-proper-continuant-part-at-some-time p q) + (exists (t) + (and (exists-at p t) (exists-at q t) + (has-proper-continuant-part p q t)))))) + + + (cl:comment "located-in at all times [vdo-1]" + (forall (p q) + (iff (located-in-at-all-times p q) + (and (exists (t) (and (located-in p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (located-in p q t))))))) + + + (cl:comment "concretizes at all times [uge-1]" + (forall (p q) + (iff (concretizes-at-all-times p q) + (and (exists (t) (and (concretizes p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (concretizes p q t))))))) + + + (cl:comment "location-of at all times [imi-1]" + (forall (p q) + (iff (location-of-at-all-times p q) + (and (exists (t) (and (location-of p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (location-of p q t))))))) + + + (cl:comment "is-carrier-of at all times [fya-1]" + (forall (p q) + (iff (is-carrier-of-at-all-times p q) + (and (exists (t) (and (is-carrier-of p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (is-carrier-of p q t))))))) + + + (cl:comment "member-part-of at all times [maf-1]" + (forall (p q) + (iff (member-part-of-at-all-times p q) + (and (exists (t) (and (member-part-of p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (member-part-of p q t))))))) + + + (cl:comment "has-member-part at all times [xwi-1]" + (forall (p q) + (iff (has-member-part-at-all-times p q) + (and (exists (t) (and (has-member-part p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (has-member-part p q t))))))) + + + (cl:comment "has-participant at all times [wyo-1]" + (forall (p q) + (iff (has-participant-at-all-times p q) + (and (exists (t) (and (has-participant p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (has-participant p q t))))))) + + + (cl:comment "participates-in at all times [ghl-1]" + (forall (p q) + (iff (participates-in-at-all-times p q) + (and (exists (t) (and (participates-in p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (participates-in p q t))))))) + + + (cl:comment "is-concretized-by at all times [qhq-1]" + (forall (p q) + (iff (is-concretized-by-at-all-times p q) + (and (exists (t) (and (is-concretized-by p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (is-concretized-by p q t))))))) + + + (cl:comment "material-basis-of at all times [scx-1]" + (forall (p q) + (iff (material-basis-of-at-all-times p q) + (and (exists (t) (and (material-basis-of p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (material-basis-of p q t))))))) + + + (cl:comment "continuant-part-of at all times [ztt-1]" + (forall (p q) + (iff (continuant-part-of-at-all-times p q) + (and (exists (t) (and (continuant-part-of p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (continuant-part-of p q t))))))) + + + (cl:comment "has-material-basis at all times [qdl-1]" + (forall (p q) + (iff (has-material-basis-at-all-times p q) + (and (exists (t) (and (has-material-basis p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (has-material-basis p q t))))))) + + + (cl:comment "has-continuant-part at all times [uhy-1]" + (forall (p q) + (iff (has-continuant-part-at-all-times p q) + (and (exists (t) (and (has-continuant-part p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (has-continuant-part p q t))))))) + + + (cl:comment "generically-depends-on at all times [wie-1]" + (forall (p q) + (iff (generically-depends-on-at-all-times p q) + (and + (exists (t) (and (generically-depends-on p q t) (exists-at p t))) + (forall (t) (if (exists-at p t) (generically-depends-on p q t))))))) + + + (cl:comment "occupies-spatial-region at all times [tpr-1]" + (forall (p q) + (iff (occupies-spatial-region-at-all-times p q) + (and + (exists (t) (and (occupies-spatial-region p q t) (exists-at p t))) + (forall (t) + (if (exists-at p t) (occupies-spatial-region p q t))))))) + + + (cl:comment "spatially-projects-onto at all times [ogh-1]" + (forall (p q) + (iff (spatially-projects-onto-at-all-times p q) + (and + (exists (t) (and (spatially-projects-onto p q t) (exists-at p t))) + (forall (t) + (if (exists-at p t) (spatially-projects-onto p q t))))))) + + + (cl:comment "proper-continuant-part-of at all times [jiz-1]" + (forall (p q) + (iff (proper-continuant-part-of-at-all-times p q) + (and + (exists (t) + (and (proper-continuant-part-of p q t) (exists-at p t))) + (forall (t) + (if (exists-at p t) (proper-continuant-part-of p q t))))))) + + + (cl:comment "has-proper-continuant-part at all times [mxe-1]" + (forall (p q) + (iff (has-proper-continuant-part-at-all-times p q) + (and + (exists (t) + (and (has-proper-continuant-part p q t) (exists-at p t))) + (forall (t) + (if (exists-at p t) (has-proper-continuant-part p q t))))))) + +))) \ No newline at end of file diff --git a/src/owl/temporal extensions/temporalized relations/prover9/temporalized-relations.p9 b/src/owl/temporal extensions/temporalized relations/prover9/temporalized-relations.p9 new file mode 100644 index 0000000..f573572 --- /dev/null +++ b/src/owl/temporal extensions/temporalized relations/prover9/temporalized-relations.p9 @@ -0,0 +1,116 @@ +% BFO 2020 Axiomatization of temporalized relations, generated 2024/01/08 +% Author: Alan Ruttenberg - alanruttenberg@gmail.com +% The most recent version of this file will always be in the GitHub repository https://github.com/bfo-ontology/bfo-2020 +% This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/ + +% located-in at some time +all p all q ((locatedInAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (locatedIn(p,q,t)))))) # label("located-in-at-some-time") . + +% concretizes at some time +all p all q ((concretizesAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (concretizes(p,q,t)))))) # label("concretizes-at-some-time") . + +% location-of at some time +all p all q ((locationOfAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (locationOf(p,q,t)))))) # label("location-of-at-some-time") . + +% is-carrier-of at some time +all p all q ((isCarrierOfAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (isCarrierOf(p,q,t)))))) # label("is-carrier-of-at-some-time") . + +% member-part-of at some time +all p all q ((memberPartOfAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (memberPartOf(p,q,t)))))) # label("member-part-of-at-some-time") . + +% has-member-part at some time +all p all q ((hasMemberPartAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (hasMemberPart(p,q,t)))))) # label("has-member-part-at-some-time") . + +% has-participant at some time +all p all q ((hasParticipantAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (hasParticipant(p,q,t)))))) # label("has-participant-at-some-time") . + +% participates-in at some time +all p all q ((participatesInAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (participatesIn(p,q,t)))))) # label("participates-in-at-some-time") . + +% rdf:type is interpreted as meaning an instance is a given type whenever it exists, and that the instance exists at some point. +all c all i ((rdfType(c,i)) <-> (((all t ((existsAt(i,t)) -> (instanceOf(i,c,t)))) & (exists t (existsAt(i,t)))))) # label("rdf-type-interpretation") . + +% is-concretized-by at some time +all p all q ((isConcretizedByAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (isConcretizedBy(p,q,t)))))) # label("is-concretized-by-at-some-time") . + +% material-basis-of at some time +all p all q ((materialBasisOfAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (materialBasisOf(p,q,t)))))) # label("material-basis-of-at-some-time") . + +% continuant-part-of at some time +all p all q ((continuantPartOfAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (continuantPartOf(p,q,t)))))) # label("continuant-part-of-at-some-time") . + +% has-material-basis at some time +all p all q ((hasMaterialBasisAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (hasMaterialBasis(p,q,t)))))) # label("has-material-basis-at-some-time") . + +% has-continuant-part at some time +all p all q ((hasContinuantPartAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (hasContinuantPart(p,q,t)))))) # label("has-continuant-part-at-some-time") . + +% generically-depends-on at some time +all p all q ((genericallyDependsOnAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (genericallyDependsOn(p,q,t)))))) # label("generically-depends-on-at-some-time") . + +% occupies-spatial-region at some time +all p all q ((occupiesSpatialRegionAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (occupiesSpatialRegion(p,q,t)))))) # label("occupies-spatial-region-at-some-time") . + +% spatially-projects-onto at some time +all p all q ((spatiallyProjectsOntoAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (spatiallyProjectsOnto(p,q,t)))))) # label("spatially-projects-onto-at-some-time") . + +% proper-continuant-part-of at some time +all p all q ((properContinuantPartOfAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (properContinuantPartOf(p,q,t)))))) # label("proper-continuant-part-of-at-some-time") . + +% has-proper-continuant-part at some time +all p all q ((hasProperContinuantPartAtSomeTime(p,q)) <-> (exists t (((existsAt(p,t)) & (existsAt(q,t)) & (hasProperContinuantPart(p,q,t)))))) # label("has-proper-continuant-part-at-some-time") . + +% located-in at all times +all p all q ((locatedInAtAllTimes(p,q)) <-> (((exists t (((locatedIn(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (locatedIn(p,q,t))))))) # label("located-in-at-all-times") . + +% concretizes at all times +all p all q ((concretizesAtAllTimes(p,q)) <-> (((exists t (((concretizes(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (concretizes(p,q,t))))))) # label("concretizes-at-all-times") . + +% location-of at all times +all p all q ((locationOfAtAllTimes(p,q)) <-> (((exists t (((locationOf(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (locationOf(p,q,t))))))) # label("location-of-at-all-times") . + +% is-carrier-of at all times +all p all q ((isCarrierOfAtAllTimes(p,q)) <-> (((exists t (((isCarrierOf(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (isCarrierOf(p,q,t))))))) # label("is-carrier-of-at-all-times") . + +% member-part-of at all times +all p all q ((memberPartOfAtAllTimes(p,q)) <-> (((exists t (((memberPartOf(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (memberPartOf(p,q,t))))))) # label("member-part-of-at-all-times") . + +% has-member-part at all times +all p all q ((hasMemberPartAtAllTimes(p,q)) <-> (((exists t (((hasMemberPart(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (hasMemberPart(p,q,t))))))) # label("has-member-part-at-all-times") . + +% has-participant at all times +all p all q ((hasParticipantAtAllTimes(p,q)) <-> (((exists t (((hasParticipant(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (hasParticipant(p,q,t))))))) # label("has-participant-at-all-times") . + +% participates-in at all times +all p all q ((participatesInAtAllTimes(p,q)) <-> (((exists t (((participatesIn(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (participatesIn(p,q,t))))))) # label("participates-in-at-all-times") . + +% is-concretized-by at all times +all p all q ((isConcretizedByAtAllTimes(p,q)) <-> (((exists t (((isConcretizedBy(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (isConcretizedBy(p,q,t))))))) # label("is-concretized-by-at-all-times") . + +% material-basis-of at all times +all p all q ((materialBasisOfAtAllTimes(p,q)) <-> (((exists t (((materialBasisOf(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (materialBasisOf(p,q,t))))))) # label("material-basis-of-at-all-times") . + +% continuant-part-of at all times +all p all q ((continuantPartOfAtAllTimes(p,q)) <-> (((exists t (((continuantPartOf(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (continuantPartOf(p,q,t))))))) # label("continuant-part-of-at-all-times") . + +% has-material-basis at all times +all p all q ((hasMaterialBasisAtAllTimes(p,q)) <-> (((exists t (((hasMaterialBasis(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (hasMaterialBasis(p,q,t))))))) # label("has-material-basis-at-all-times") . + +% has-continuant-part at all times +all p all q ((hasContinuantPartAtAllTimes(p,q)) <-> (((exists t (((hasContinuantPart(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (hasContinuantPart(p,q,t))))))) # label("has-continuant-part-at-all-times") . + +% generically-depends-on at all times +all p all q ((genericallyDependsOnAtAllTimes(p,q)) <-> (((exists t (((genericallyDependsOn(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (genericallyDependsOn(p,q,t))))))) # label("generically-depends-on-at-all-times") . + +% occupies-spatial-region at all times +all p all q ((occupiesSpatialRegionAtAllTimes(p,q)) <-> (((exists t (((occupiesSpatialRegion(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (occupiesSpatialRegion(p,q,t))))))) # label("occupies-spatial-region-at-all-times") . + +% spatially-projects-onto at all times +all p all q ((spatiallyProjectsOntoAtAllTimes(p,q)) <-> (((exists t (((spatiallyProjectsOnto(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (spatiallyProjectsOnto(p,q,t))))))) # label("spatially-projects-onto-at-all-times") . + +% proper-continuant-part-of at all times +all p all q ((properContinuantPartOfAtAllTimes(p,q)) <-> (((exists t (((properContinuantPartOf(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (properContinuantPartOf(p,q,t))))))) # label("proper-continuant-part-of-at-all-times") . + +% has-proper-continuant-part at all times +all p all q ((hasProperContinuantPartAtAllTimes(p,q)) <-> (((exists t (((hasProperContinuantPart(p,q,t)) & (existsAt(p,t))))) & (all t ((existsAt(p,t)) -> (hasProperContinuantPart(p,q,t))))))) # label("has-proper-continuant-part-at-all-times") . +