Generating DL existential restrictions from CLIF is incomplete #52
Description
given:
(cl-text http://example.org
(forall (x)
(if
(nucleus x)
(exists (y)
(and (cell y)
(part_of x y)))
)
)
)I would expect
SubClassOf x ObjectSomeValuesFrom(part_of cell))
however, this is weakened to
SubClassOf x ObjectSomeValuesFrom(part_of Thing))
This is what the XML is:
<SubClassOf>
<Class IRI="nucleus"/>
<ObjectSomeValuesFrom>
<ObjectProperty IRI="part_of"/>
<Class abbreviatedIRI="owl:Thing"/>
</ObjectSomeValuesFrom>
</SubClassOf>The initial formula is being parsed and transformed into an equivalent form:
∀z[(~nucleus(z) | ∃y[(cell(y) & part_of(z,y))]]
This is then converted to Conjunctive Normal Form (CNF):
∀z[∃y[((~nucleus(z) | cell(y)) & (~nucleus(z) | part_of(z,y)))]]
This is all OK
The system then prunes this into two separate axioms:
∀z[∃y[(~nucleus(z) | cell(y))]]
∀z[∃y[(~nucleus(z) | part_of(z,y))]]
These are then treated independently but I think they need to be treated together?
The full trace:
024-09-27 16:50:17,850 macleod.Filemgt INFO Config file read: /Users/cjm/macleod/macleod_mac.conf
2024-09-27 16:50:17,850 macleod.Filemgt INFO Logging configuration file read: /Users/cjm/macleod/logging.conf
2024-09-27 16:50:17,851 macleod.Filemgt DEBUG Started logging with MacleodConfigParser
2024-09-27 16:50:17,851 macleod.scripts.parser INFO Called script clif_to_owl
ELIMINATING CONDITIONALS True
2024-09-27 16:50:17,852 macleod.scripts.parser INFO Starting to parse ../macleod/t.clif
2024-09-27 16:50:17,860 macleod.Ontology INFO Found 2 axioms in /Users/cjm/repos/macleod/t.clif
Axiom: \forall x,y\;[(~p(x,y) | q(x,y))] from /Users/cjm/repos/macleod/t.clif
2024-09-27 16:50:17,860 macleod.logical.axiom DEBUG Starting Axiom: \forall x,y\;[(~p(x,y) | q(x,y))]
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Function Free: \forall x,y\;[(~p(x,y) | q(x,y))]
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Unique Variables: \forall z,y\;[(~p(z,y) | q(z,y))]
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Distributed Negation: \forall z,y\;[(~p(z,y) | q(z,y))]
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Term: p(z,y)
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Term: q(z,y)
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Term: ~p(z,y)
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Term: (~p(z,y) | q(z,y))
2024-09-27 16:50:17,861 macleod.logical.connective DEBUG Coalesced Called: (~p(z,y) | q(z,y))
2024-09-27 16:50:17,861 macleod.logical.axiom DEBUG Coalesced Term: (~p(z,y) | q(z,y))
2024-09-27 16:50:17,862 macleod.logical.connective DEBUG Rescope Called: (~p(z,y) | q(z,y))
2024-09-27 16:50:17,862 macleod.logical.connective DEBUG No Quantifier children: (~p(z,y) | q(z,y))
2024-09-27 16:50:17,862 macleod.logical.axiom DEBUG Rescoped Term: (~p(z,y) | q(z,y))
2024-09-27 16:50:17,862 macleod.logical.axiom DEBUG Term: \forall z,y\;[(~p(z,y) | q(z,y))]
2024-09-27 16:50:17,862 macleod.logical.axiom DEBUG Duplicated Prenex: \forall z,y\;[(~p(z,y) | q(z,y))]
2024-09-27 16:50:17,862 macleod.logical.axiom DEBUG Prenex Form: \forall z,y\;[(~p(z,y) | q(z,y))]
2024-09-27 16:50:17,862 macleod.logical.axiom DEBUG CNF Form: \forall z,y\;[(~p(z,y) | q(z,y))]
FF-PCNF: \forall z,y\;[(~p(z,y) | q(z,y))]
2024-09-27 16:50:17,862 macleod.dl.utilities DEBUG Adding to the quantifier
+ yielded: \forall z,y\;[(~p(z,y) | q(z,y))]
- pattern subproperty
Axiom: \forall x\;[(~nucleus(x) | \exists y\;[(cell(y) & part_of(x,y))])] from /Users/cjm/repos/macleod/t.clif
2024-09-27 16:50:17,862 macleod.logical.axiom DEBUG Starting Axiom: \forall x\;[(~nucleus(x) | \exists y\;[(cell(y) & part_of(x,y))])]
2024-09-27 16:50:17,863 macleod.logical.axiom DEBUG Function Free: \forall x\;[(~nucleus(x) | \exists y\;[(cell(y) & part_of(x,y))])]
2024-09-27 16:50:17,863 macleod.logical.axiom DEBUG Unique Variables: \forall z\;[(~nucleus(z) | \exists y\;[(cell(y) & part_of(z,y))])]
2024-09-27 16:50:17,863 macleod.logical.axiom DEBUG Distributed Negation: \forall z\;[(~nucleus(z) | \exists y\;[(cell(y) & part_of(z,y))])]
2024-09-27 16:50:17,863 macleod.logical.axiom DEBUG Term: part_of(z,y)
2024-09-27 16:50:17,863 macleod.logical.axiom DEBUG Term: cell(y)
2024-09-27 16:50:17,863 macleod.logical.axiom DEBUG Term: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,863 macleod.logical.connective DEBUG Coalesced Called: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Coalesced Term: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG Rescope Called: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG No Quantifier children: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Rescoped Term: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Term: nucleus(z)
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Term: \exists y\;[(cell(y) & part_of(z,y))]
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Term: ~nucleus(z)
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Term: (~nucleus(z) | \exists y\;[(cell(y) & part_of(z,y))])
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG Coalesced Called: (~nucleus(z) | \exists y\;[(cell(y) & part_of(z,y))])
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Coalesced Term: (~nucleus(z) | \exists y\;[(cell(y) & part_of(z,y))])
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG Rescope Called: (~nucleus(z) | \exists y\;[(cell(y) & part_of(z,y))])
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG Rescoping: Single quantifier
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG Rescope Called: ((cell(y) & part_of(z,y)) | ~nucleus(z))
2024-09-27 16:50:17,864 macleod.logical.connective DEBUG No Quantifier children: ((cell(y) & part_of(z,y)) | ~nucleus(z))
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Rescoped Term: \exists y\;[((cell(y) & part_of(z,y)) | ~nucleus(z))]
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Term: \forall z\;[\exists y\;[((cell(y) & part_of(z,y)) | ~nucleus(z))]]
2024-09-27 16:50:17,864 macleod.logical.axiom DEBUG Duplicated Prenex: \forall z\;[\exists y\;[((cell(y) & part_of(z,y)) | ~nucleus(z))]]
2024-09-27 16:50:17,865 macleod.logical.axiom DEBUG Prenex Form: \forall z\;[\exists y\;[((cell(y) & part_of(z,y)) | ~nucleus(z))]]
2024-09-27 16:50:17,865 macleod.logical.connective DEBUG ((cell(y) & part_of(z,y)) | ~nucleus(z)) (<class 'macleod.logical.connective.Disjunction'>) is NOT in ONF because it contains a conjunction ((cell(y) & part_of(z,y)))
2024-09-27 16:50:17,865 macleod.logical.connective DEBUG ((cell(y) & part_of(z,y)) | ~nucleus(z)) (<class 'macleod.logical.connective.Disjunction'>) is NOT in ONF because it contains a conjunction ((cell(y) & part_of(z,y)))
2024-09-27 16:50:17,865 macleod.logical.connective DEBUG ((cell(y) & part_of(z,y)) | ~nucleus(z)) (<class 'macleod.logical.connective.Disjunction'>) is NOT in ONF because it contains a conjunction ((cell(y) & part_of(z,y)))
2024-09-27 16:50:17,865 macleod.logical.connective DEBUG Disjunction: ((cell(y) & part_of(z,y)) | ~nucleus(z)) is not in CNF
2024-09-27 16:50:17,865 macleod.logical.connective DEBUG Culprit is nested conjunction: (cell(y) & part_of(z,y))
2024-09-27 16:50:17,865 macleod.logical.connective DEBUG ~nucleus(z) -- (cell(y) & part_of(z,y))
2024-09-27 16:50:17,866 macleod.logical.axiom DEBUG CNF Form: \forall z\;[\exists y\;[((~nucleus(z) | cell(y)) & (~nucleus(z) | part_of(z,y)))]]
FF-PCNF: \forall z\;[\exists y\;[((~nucleus(z) | cell(y)) & (~nucleus(z) | part_of(z,y)))]]
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Adding to the quantifier
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Adding to the quantifier
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Adding to the quantifier
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Adding to the quantifier
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Pruned Conjunct:(~nucleus(z) | cell(y))
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Observed Variables: {'y', 'z'}
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Starting Prenex: [\forall z\;[\exists y\;[Null(null)]], \exists y\;[Null(null)]]
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Seen Variables: {'y', 'z'} Current Variables: {'z'}
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Seen Variables: {'y', 'z'} Current Variables: {'y'}
2024-09-27 16:50:17,866 macleod.dl.utilities DEBUG Pruned Axiom: \forall z\;[\exists y\;[(~nucleus(z) | cell(y))]]
+ yielded: \forall z\;[\exists y\;[(~nucleus(z) | cell(y))]]
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Adding to the quantifier
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Adding to the quantifier
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Pruned Conjunct:(~nucleus(z) | part_of(z,y))
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Observed Variables: {'y', 'z'}
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Starting Prenex: [\forall z\;[\exists y\;[Null(null)]], \exists y\;[Null(null)]]
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Seen Variables: {'y', 'z'} Current Variables: {'z'}
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Seen Variables: {'y', 'z'} Current Variables: {'y'}
2024-09-27 16:50:17,867 macleod.dl.utilities DEBUG Pruned Axiom: \forall z\;[\exists y\;[(~nucleus(z) | part_of(z,y))]]