RacerPro 2.0 preview : Explanation component:
RacerPro 2.0 Preview features some new explanation and ontology debugging mechanisms in order to trace down inconsistencies in ontologies. For example, an ontology can be checked for inconsistent (unsatisfiable) concepts, and an explanation describing the source of each inconsistency is generated.
Example session through RacerPorter
Please start up RacerPorter and load the ontology "People and Pets" from the examples folder. Enter (check-ontology "~/KBs/people+pets.owl") into the shell tab. The complete session is prompted below.
[9] ? (check-ontology "~/KBs/people+pets.owl")
Reading ontology ~/KBs/people+pets.owl...
Duplicate definition (or |http://cohse.semanticweb.org/ontologies/people#animal| (some |
http://cohse.semanticweb.org/ontologies/people#part_of| |http://cohse.semanticweb.org/ontologies/people#animal|)) for |
http://cohse.semanticweb.org/ontologies/people#Axiom_2| transformed into two GCIs. (@ character position 18760)
Reading ontology ~/KBs/people+pets.owl done.
Concept (|http://cohse.semanticweb.org/ontologies/people#animal|) causes a cycle in TBox ~/KBs/people+pets.owl.
Concept (|http://cohse.semanticweb.org/ontologies/people#plant|) causes a cycle in TBox ~/KBs/people+pets.owl.
Concept (|http://cohse.semanticweb.org/ontologies/people#Axiom_2|) causes a cycle in TBox ~/KBs/people+pets.owl
[9] > ((:incoherent-concept
http://cohse.semanticweb.org/ontologies/people#mad_cow
((:ref-ind
http://cohse.semanticweb.org/ontologies/people#mad_cow)
(:inference-step
:assertion
(:ref-ind http://cohse.semanticweb.org/ontologies/people#cow)
:axiom
(implies
http://cohse.semanticweb.org/ontologies/people#cow
http://cohse.semanticweb.org/ontologies/people#vegetarian))
(:inference-step
:assertion
(:ref-ind
http://cohse.semanticweb.org/ontologies/people#mad_cow)
:axiom
(equivalent
http://cohse.semanticweb.org/ontologies/people#mad_cow
(and
(some
http://cohse.semanticweb.org/ontologies/people#eats
(and
(some
http://cohse.semanticweb.org/ontologies/people#part_of
http://cohse.semanticweb.org/ontologies/people#sheep)
http://cohse.semanticweb.org/ontologies/people#brain))
http://cohse.semanticweb.org/ontologies/people#cow)))
(:inference-step
:assertion
(:ref-ind
http://cohse.semanticweb.org/ontologies/people#vegetarian)
:axiom
(equivalent
http://cohse.semanticweb.org/ontologies/people#vegetarian
(and
(all
http://cohse.semanticweb.org/ontologies/people#eats
(all
http://cohse.semanticweb.org/ontologies/people#part_of
(not
http://cohse.semanticweb.org/ontologies/people#animal)))
(all
http://cohse.semanticweb.org/ontologies/people#eats
(not
http://cohse.semanticweb.org/ontologies/people#animal))
http://cohse.semanticweb.org/ontologies/people#animal))))))
This output indicates the reason for the inconsitency of the "mad_cow" concept in the people+pets ontology. An instance of "mad_cow" is, be definition of "mad_cow", also a cow. Since "cows" are vegetarians by definition:
:axiom
(implies
http://cohse.semanticweb.org/ontologies/people#cow
http://cohse.semanticweb.org/ontologies/people#vegetarian))
and since "vegatarians" only eat things which are not animals, and only eat parts of "non-animals":
:axiom
(equivalent
http://cohse.semanticweb.org/ontologies/people#vegetarian
(and
(all
http://cohse.semanticweb.org/ontologies/people#eats
(all
http://cohse.semanticweb.org/ontologies/people#part_of
(not
http://cohse.semanticweb.org/ontologies/people#animal)))
(all
http://cohse.semanticweb.org/ontologies/people#eats
(not
http://cohse.semanticweb.org/ontologies/people#animal))
http://cohse.semanticweb.org/ontologies/people#animal))))))
but "mad_cows" are defined as eating brains which are part of "sheep",
:axiom
(equivalent
http://cohse.semanticweb.org/ontologies/people#mad_cow
(and
(some
http://cohse.semanticweb.org/ontologies/people#eats
(and
(some
http://cohse.semanticweb.org/ontologies/people#part_of
http://cohse.semanticweb.org/ontologies/people#sheep)
http://cohse.semanticweb.org/ontologies/people#brain))
http://cohse.semanticweb.org/ontologies/people#cow))
there can be no "mad cows".
Also, an ABox can be checked for sources of inconsistencies as follows:
[13] ? (owl-read-file "~/KBs/people+pets.owl")
Reading ontology ~/KBs/people+pets.owl...
Duplicate definition (or |http://cohse.semanticweb.org/ontologies/people#animal| (some |
http://cohse.semanticweb.org/ontologies/people#part_of| |http://cohse.semanticweb.org/ontologies/people#animal|)) for |
http://cohse.semanticweb.org/ontologies/people#Axiom_2| transformed into two GCIs. (@ character position 18760)
Reading ontology ~/KBs/people+pets.owl done.
[13] > ~/KBs/people+pets.owl
[14] ? (instance maddy #!:mad_cow)
[14] > :OKAY
[15] ? (check-abox-coherence)
Concept (|http://cohse.semanticweb.org/ontologies/people#animal|) causes a cycle in TBox ~/KBs/people+pets.owl.
Concept (|http://cohse.semanticweb.org/ontologies/people#plant|) causes a cycle in TBox ~/KBs/people+pets.owl.
Concept (|http://cohse.semanticweb.org/ontologies/people#Axiom_2|) causes a cycle in TBox ~/KBs/people+pets.owl
[15] > (NIL
((:inference-step
:assertion
(maddy #!:cow)
:axiom
(implies #!:cow #!:vegetarian))
(maddy #!:mad_cow)
(:inference-step
:assertion
(maddy #!:vegetarian)
:axiom
(equivalent
#!:vegetarian
(and
(all #!:eats (all #!:part_of (not #!:animal)))
(all #!:eats (not #!:animal))
#!:animal)))
(:inference-step
:assertion
(maddy #!:mad_cow)
:axiom
(equivalent
#!:mad_cow
(and
(some #!:eats (and (some #!:part_of #!:sheep) #!:brain))
#!:cow)))
(:inference-step
:assertion
(0 #!:sheep)
:axiom
(implies #!:sheep (and (all #!:eats #!:grass) #!:animal))
:provenance
((:added-gci #!:animal :type :primitive-det)))
(:inference-step
:assertion
(maddy (all #!:eats (all #!:part_of (not #!:animal))))
:domain
#!:animal)
(:inference-step
:assertion
(maddy
(some #!:eats (and (some #!:part_of #!:sheep) #!:brain)))
:domain
#!:animal)
(:inference-step
:assertion
(0 (all #!:part_of (not #!:animal)))
:domain
(OR (ALL #!:part_of (NOT #!:animal)) #!:Axiom_2))
(:inference-step
:assertion
(0 (some #!:part_of #!:sheep))
:domain
(OR (ALL #!:part_of (NOT #!:animal)) #!:Axiom_2))))