Closed mereolog closed 1 year ago
The CL axiomatisation uses the 'distinct' predicate:
https://github.com/BFO-ontology/BFO-2020/blob/5eed4772c6515856c4d4be2097976856f80b18ea/21838-2/common-logic/universal-declaration.cl#L629-L640
Note that CL does not provide any semantics for this predicate, so if the intention was to convey the same constraint as in:
https://github.com/BFO-ontology/BFO-2020/blob/5eed4772c6515856c4d4be2097976856f80b18ea/21838-2/prover9/universal-declaration.prover9#L319-L320
then you need to define the 'distinct' predicate. Otherwise, the intended meaning is not guaranteed. For example, currently, you can add to the CL axiomatisation statements like: (= continuant material-entity) and still get a consistent theory.
(= continuant material-entity)
Yes, just caught that earlier today. It's fixed now, in 2c034b0c56fc16b6dc03dd9a4d3ca7a156f6bbe7
The CL axiomatisation uses the 'distinct' predicate:
https://github.com/BFO-ontology/BFO-2020/blob/5eed4772c6515856c4d4be2097976856f80b18ea/21838-2/common-logic/universal-declaration.cl#L629-L640
Note that CL does not provide any semantics for this predicate, so if the intention was to convey the same constraint as in:
https://github.com/BFO-ontology/BFO-2020/blob/5eed4772c6515856c4d4be2097976856f80b18ea/21838-2/prover9/universal-declaration.prover9#L319-L320
then you need to define the 'distinct' predicate. Otherwise, the intended meaning is not guaranteed. For example, currently, you can add to the CL axiomatisation statements like:
(= continuant material-entity)
and still get a consistent theory.