Skip to content

Commit

Permalink
fix: Repair psr-cm+
Browse files Browse the repository at this point in the history
  • Loading branch information
ngrewe committed Feb 18, 2024
1 parent 25ad88b commit 7f5a6c1
Showing 1 changed file with 48 additions and 43 deletions.
91 changes: 48 additions & 43 deletions src/test/clojure/de/halbordnung/ontologies/tqme/cq.clj
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
[clojure.test]
)
[:use clojure.test]
(:import (org.semanticweb.owlapi.reasoner OWLReasoner)))
(:import (org.semanticweb.owlapi.reasoner InconsistentOntologyException OWLReasoner)))

(def to nil)
(defn createtestontology []
Expand Down Expand Up @@ -35,7 +35,11 @@

(defn satisfiable? [ontology expr]
(.flush ^OWLReasoner (r/reasoner ontology))
(.isSatisfiable ^OWLReasoner (r/reasoner ontology) expr))
(try
(.isSatisfiable ^OWLReasoner (r/reasoner ontology) expr)
(catch InconsistentOntologyException e false)
)
)

(use-fixtures :each tqme-fixture)
(use-fixtures :once write-tqme)
Expand Down Expand Up @@ -108,57 +112,58 @@
"A mammal that at some time does not participate in a birth process → OK"))

(deftest psr_cm+
(o/owl-class to "brain"
:super b/material_entity) (let
[has-brain (o/object-property to "has-brain"
:super b/has_continuant_part_at_all_times
:range "brain"
:characteristic :functional)

part-of-brain (o/object-property to "part-of-brain"
:super b/continuant_part_of_at_all_times
:domain "brain"
:characteristic :inversefunctional)
ventricle (o/owl-class to "ventricle"
:super (o/owl-and to b/material_entity
(c/perm-spec to (o/owl-some to part-of-brain "brain")))) human (o/owl-class to "human"
:super (o/owl-and to b/material_entity
(c/perm-spec to (o/owl-some to has-brain "brain"))))

joes-brain (o/individual to "joes-brain"
:type "brain")

other-brain (o/individual to "other-brain"
:type "brain"
:different joes-brain)

joe (o/individual to "joe"
:type human
:fact (o/fact to has-brain joes-brain))

p1 (o/individual to "phase1"
:type c/phase
:fact (o/fact to c/phase-of joe))
mrx (o/individual to "mrx"
:fact (o/fact to c/has-phase p1)
:comment "Mr X should in fact be identical with Joe")

error-fact (o/fact to has-brain other-brain)]
(def brain (o/owl-class to "brain"
:super b/material_entity)) (let
[has-brain (o/object-property to "has-brain"
:super b/has_continuant_part_at_all_times
:range brain
:characteristic :functional)

part-of-brain (o/object-property to "part-of-brain"
:super b/continuant_part_of_at_all_times
:range brain
:characteristic :inversefunctional)
ventricle (o/owl-class to "ventricle"
:super (o/owl-and b/material_entity
(c/perm-spec to (o/owl-some part-of-brain brain))))
human (o/owl-class to "human"
:super (o/owl-and b/material_entity
(c/perm-spec to (o/owl-some has-brain brain))))

joes-brain (o/individual to "joes-brain"
:type brain)

other-brain (o/individual to "other-brain"
:type brain
:different joes-brain)

joe (o/individual to "joe"
:type human
:fact (o/fact has-brain joes-brain))

p1 (o/individual to "phase1"
:type c/phase
:fact (o/fact c/phase-of joe))
mrx (o/individual to "mrx"
:fact (o/fact c/has-phase p1)
:comment "Mr X should in fact be identical with Joe")

]
(is (r/consistent? to)
"Consistent before bad axiom")

(o/with-probe-axioms to
[a (o/add-fact to mrx error-fact)]
(o/add-fact to mrx (o/fact has-brain other-brain))

(is (not (r/consistent? to))
"There is a time in which Joe does not have his original brain → owl:Nothing"))

;; Sanity check: Were the probe axioms really removed?
(is (r/consistent? to))
(is (not (satisfiable? to (o/owl-and to ventricle
(o/! to
(o/owl-some to part-of-brain "brain"))
(o/owl-some to part-of-brain "brain"))))
(is (not (satisfiable? to (o/owl-and ventricle
(o/!
(o/owl-some part-of-brain brain))
(o/owl-some part-of-brain brain))))
"A brain ventricle that is part of a human brain at some time and that is not part of any human brain at another time → owl:Nothing")

;; We have a third example here but that's essentially negation of the entire scope, so we don't do it.
Expand Down

0 comments on commit 7f5a6c1

Please sign in to comment.