Post by Eleni Tsouloucha (7 October 2025)
P106 is composed of (forms part of)
P106(x,y) ¬P106(y,x)
- missing implication should be: P106(x,y) ⇒¬P106(y,x)
P132 spatiotemporally overlaps with
P132(x,y) ⇒ E92(x)
P132(x,y) ⇒ E92(y)
P132(x,y) ⇒ P132(y,x)
P132(x,y) ⇒ P132 (x,y)
P132(x,x)
Marked in yellow is a tautology and can be deleted
P133 is spatiotemporally separated from
P133(x,y) ⇒ E92(x)
P133(x,y) ⇒ E92(y)
P133(x,y) ⇒ P133(y,x)
P133(x,y) ⇒ P133(x,y)
¬P133(x,x)
Marked in yellow is a tautology and can be deleted
P200 has complete copy (is complete copy of)
P200(y,x) ⇒ E25(y)
should be P200(x,y) ⇒ E25(y)
P197 covered parts of (was partially covered by)
The full path is not expressed in the FOL
Christian-Emil Ore (p.c.)
Full path:
E93 Presence. P161 has spatial projection (is spatial projection of): E53 Place. P121 overlaps with: E53 Place
This says that
(1) for all x,y,z if P161(x,z) and P121(z,y) then we have P197(x,y)
or if we move the implicit universal quantifier for z inside, then it will become existential quantifier since ∀x( A(x) ⇒ B) is equivalent to (∃xA(x)) ⇒ B.
(2) for all x,y if there exists at least one z such that P161(x,z) and P(121(z,y) then P197(x,y)
If we want to make things clear and readable, we add the E93(x), E53(z) , E53(y) although this is implied by P161(x,z) and P121(z,y) and P197(x,z).
The universal quantifier for z:E53 can be moved outside the implication in (1) since z does not occur (unbound) in P197(x,y)
so
[P197(x,y) ⇐ P161(x,z) ∧ P121(z,y)] ∧ (E53(y) ∧ E53(z) ∧E93(x)
There are implicit universal quantifiers x,y,z, and as I said above the for all z can be moved inside the implication and we get
[P197(x,y) ⇐ ∃x [(E53(z) ∧ (P161(x,z) ∧ P121(z,y)]] ∧ (E53(y) ∧E93(x)
or simplified in analogy with P8: P8(x,y) ⇐ (∃z) [E53(z) ∧ P7(x,z) ∧ P156i(z,y)]
P197(x,y) ⇐ ∃x [(E53(z) ∧ (P161(x,z) ∧ P121(z,y)]
Chr-Emil
The FOL for the relation between P197 and the long path it shortcuts over; namely, P197(x,y) ⇐ ∃x [(E53(z) ∧ (P161(x,z) ∧ P121(z,y)], has been accepted by editorial decision. It features in CIDOC CRM v7.4.
This was the only point for this issue that hadn't been addressed.
Issue closed