Issue proposed by Martin Doerr (p.c) -- 8 August 2024
remove all inverse labels from FOL statements. Use reverseorder of arguments instead.
Motivation for proposal:
a) confusing ambiguity
b) missing semantics of the inverse label in FOL
c) incompatibility with KR models that do not have two names for one property
Nb.
A quick search in CRMbase 7_2_5 after 'i(' results in 29 matches.
e.g:
P50(x,y) ⇐ (∃z) [[E10(z) ∧ P30i(x,z) ∧ P29(z,y)] ∧
¬ (∃w) [E10(w) ∧ P30i(x,w) ∧ P28(w,y) ∧ P182(z,w)]]
and
P73(x,y) ⇒ P130i(x,y)
The other way round '(y,' returns 41 matches many of which are in complex FOLs and do not represent inverse.
So the 'i'-notation is clearly used. It is better to switch the order of the arguments. It is also a question if one should switch the order in the label or just use the i. It has been discussed but no formal editorial decision exists. We should should get rid of the 'i' notation in the FOLs.
In the 60th joint meeting of the CIDOC CRM and ISO/TC46/SC4/WG9 & 53rd FRBR/LRMoo SIG, the SIG reviewed the proposal by MD & CEO to remove inverse indexes from properties in the FOL statements, and use the forward going property [PXi(x,y) ⇔ PX(y,x)] and reverse the order of the arguments instead.
There were many objections, and the SIG decided not to go through with this proposal after all.
forward-going property identifiers, whose arguments appear in the inverse form are far more difficult to read, it creates complexity for the model, at the risk of deriving illegible FOL statements, or meaningless ones (like the ones pointed to by WS –see here)
HW was assigned to WS to check:
- that the referenced inverse properties all correspond to an actual property (recall P170 and P82i)
- whether there exist any FOL axioms that mention the forward going predicate (whose arguments appear in an inversed order), rather than the inverse property predicate that should be used instead.
HW was assigned to CEO to draft a paragraph in the introduction section (part concerning the FOL expressions) about the equivalence between inverse and forward going property predicates [PXi(x,y) ⇔ PX(y,x)]
Bern, April 2025
Post by Christian-Emil Ore (6 October 2025)
Dear all,
The original idea in Issue 692 "Inverse properties in FOL" was to get rid of the use if the 'i' notation indicating the use of the inverse of a given property, as for example in the definition of P2 (page 119):
- P2: This property is a shortcut for the path from E1 CRM Entity through P41i was classified by (classified), E17 Type Assignment, P42 assigned (was assigned by) to E55 Type.
- P2(x,y) ⇐ (∃z) [E17(z)] ∧ P41i(x,z) ∧ P42(z,y)]
The suggestion was not welcomed by the SIG and as the example above shows it can be handy. The proposal is dropped and instead one should write a short text to be put into the introduction (the part about FOL formalism).
Suggestion (addition marked at page 23):
In contrast, first-order logic-based knowledge representation relies on a language for formally encoding an ontology. This language can be directly put in correspondence with semantic data modelling in a straightforward way:
- classes are named by unary predicate symbols; conventionally, we use E21 as the unary predicate symbol corresponding to class E21 Person;
- properties are named by binary predicate symbols; conventionally, we use P152 as the binary predicate symbol corresponding to property P152 has parent (is parent of).
- properties of properties, “.1 properties” are named by ternary predicate symbols; conventionally, we use P14.1 as the ternary predicate symbol corresponding to property P14.1 in the role of.
- inverse of properties are indicated using an ‘i’ after the number. So P152i is parent of (has parent) is the inverse of P152 has parent (is parent of). In the First-Order representation the arguments are swapped so P152(x,y) is equivalent to P152i(y,x).
The second part of the HW: to check if swapping arguments are used in the FOL axioms:
P5:
[P5(x,y) ∧ P5(y,z)] ⇒ P5(x,z)
P5(x,y) ⇒ ¬P5(y,x)
and all the other anti-symmetric ones. In my opinion it is ok to leave them as is. In the FOL for the fully developed paths only the inverse were used.
Best,
Christian-Emil