Issue 676: Harmonizing CRMbase logically with CRMgeo
Post by Martin Doerr (25 Feb 2024)
Dear All,
In the course of updating CRMgeo to CRM 7.2.4, there is a logical problem to solve with P168, 169, 170, which define Declarative spaces and times, but CRMbase does not have these classes.
Nevertheless, these 3 properties are designed in CRMbase not to be used for phenomenal spaces and times. Therefore I here propose to formulate this as FOL rules in CRMbase, so that no formal inconsistency will occur when using CRMgeo proper to declare the 3 properties to be restricted to instances of SP6 Declarative Place, SP7 Declarative Spacetime Volume, SP10 Declarative Time-Span, or via subproperties of P168,P169,P170.
Hence:
A)
P168(x,y) ⇒ E53(x)
P168(x,y) ⇒ E94(y)
P168(x,y) ⇒ P1i(x,y)
P168(x,y) ⇒ (¬∃z) [E92(z) ⋀ P161(z,x) ⋀ (P169 (u,z) ] Excluding the place to be a projection of a physical thing
P168(x,y) ⇒ (¬∃z) [E4(z) ⋀ P161(z,x)] Excluding the place to be a projection of an instance of E4 Period
B)
P169(x,y) ⇒ E95(x)
P169(x,y) ⇒ E92(y)
P169(x,y) ⇒ P1i(x,y)
P169(x,y) ⇒ (¬∃z)[E18(z) ⋀ P196(y,z)] Excluding STV to be defined by a physical thing
P169(x,y) ⇒ ¬ E4(y) Excluding the STV to be an instance of E4 Period
C)
P170(x,y) ⇒ E61(x)
P170(x,y) ⇒ E52(y)
P170(x, y) ⇒ P81i(x, y) ∧ P82i(x, y)
P170(x,y) ⇒ (¬∃z)[E2(z) ⋀ P4(z,y)] Excluding an instance of Temporal Entity to happen at this Time-Span
Best,
Martin
Post by Martin Doerr (25 Feb 2024)
Dear All,
From the CRMgeo side, we have two choices:
Either we declare
Q10 defines place
| Domain: E94 Space Primitive |
| Range: SP6 Declarative Place |
to be suproperty of P168i,
Q14 defines time
| Domain: SP14 Time Expression Now: E61_Time_Primitive |
| Range: SP10 Declarative Time-Span |
to be suproperty of P170,
Q16 defines spacetime volume
| Domain: SP12 Spacetime Volume Expression Now: E95_Spacetime_Primitive |
| Range: SP7 Declarative Spacetime Volume |
to be suproperty of P169,
OR:
P168(x,y) ⇒ SP6(x) (SP6_Declarative _Place)
P169(x,y) ⇒ SP7(y)
P170(x,y) ⇒ SP10(y)
All the best,
martin