From 2711535b84201ec3b98dacdfe45ece8935edbfdc Mon Sep 17 00:00:00 2001 From: Alan Ruttenberg Date: Tue, 30 Jan 2024 15:57:04 -0500 Subject: [PATCH] Establish a release notes directory and add a bit more documentation about the axiomatization release of earlier this month --- ...xiomatization-release-notes-2024-01-10.txt | 278 ++++++++++++++++++ 1 file changed, 278 insertions(+) create mode 100644 release-notes/FOL-axiomatization-release-notes-2024-01-10.txt diff --git a/release-notes/FOL-axiomatization-release-notes-2024-01-10.txt b/release-notes/FOL-axiomatization-release-notes-2024-01-10.txt new file mode 100644 index 0000000..fe2f98d --- /dev/null +++ b/release-notes/FOL-axiomatization-release-notes-2024-01-10.txt @@ -0,0 +1,278 @@ +This release updates the FOL version of BFO as captured in common logic, prover9, and typeset pdf. +Most of the axioms whose logical form changed are simplifications removing "(exists (?t) .." by +using an appropriate existing time variable. This benefits theorem provers for which there is +an extra cost for skolemization. + +The axiom inheres-in-domain-range is removed because it is a theorem. It turns out there +are many "axioms" that are actually theorems. We'll organize this better in a subsequent release. + +Most of the new axioms are of two types: +- Being explicit about the spatial regions continuant fiat boundaries occupy +- Being clear that the spatial region anything occupies doesn't ever change dimension + +The axiom all-participation-at-process-occupied-temporal-region tightens the relation between +participation and processes, ensuring that all participation happens in the temporal region +a process occupies. + +Common Logic files: 'src/common logic' +Prover 9 files: 'src/prover9' +Typeset: 'documentation/axiomatization pdfs' + +Alan Ruttenberg 2024-01-10 + +- + +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))))) +