OWLAPI：想要使用 HermiT 推理器从 ontology 中获得推断的公理

Question

我想从推理机 [HermiT] 那里得到推断的公理及其正确的解释。我在 protege 中创建了以下 ontology。

A.owl

<?xml version="1.0"?>
<!DOCTYPE rdf:RDF [
    <!ENTITY owl "http://www.w3.org/2002/07/owl#" >
    <!ENTITY xsd "http://www.w3.org/2001/XMLSchema#" >
    <!ENTITY rdfs "http://www.w3.org/2000/01/rdf-schema#" >
    <!ENTITY rdf "http://www.w3.org/1999/02/22-rdf-syntax-ns#" >
]>
<rdf:RDF xmlns="http://www.semanticweb.org/ontologies/A#"
     xml:base="http://www.semanticweb.org/ontologies/A"
     xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
     xmlns:owl="http://www.w3.org/2002/07/owl#"
     xmlns:xsd="http://www.w3.org/2001/XMLSchema#"
     xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#">
    <owl:Ontology rdf:about="http://www.semanticweb.org/ontologies/A"/>
    <!-- 
    ///////////////////////////////////////////////////////////////////////////////////////
    //
    // Classes
    //
    ///////////////////////////////////////////////////////////////////////////////////////
     -->
    <!-- http://www.semanticweb.org/ontologies/A#A -->
    <owl:Class rdf:about="http://www.semanticweb.org/ontologies/A#A">
        <rdfs:subClassOf rdf:resource="http://www.semanticweb.org/ontologies/A#B"/>
    </owl:Class>
    <!-- http://www.semanticweb.org/ontologies/A#B -->
    <owl:Class rdf:about="http://www.semanticweb.org/ontologies/A#B">
        <owl:equivalentClass rdf:resource="http://www.semanticweb.org/ontologies/A#C"/>
    </owl:Class>
    <!-- http://www.semanticweb.org/ontologies/A#C -->
    <owl:Class rdf:about="http://www.semanticweb.org/ontologies/A#C"/>
</rdf:RDF>
<!-- Generated by the OWL API (version 3.5.1) http://owlapi.sourceforge.net -->

以下是我的 Java 代码 :-

//Some work done to load ontology
ReasonerFactory factory = new ReasonerFactory();
Reasoner reasoner = new Reasoner(reasonerConf, owlOntology);
BlackBoxExplanation explain = new BlackBoxExplanation(owlOntology, factory, reasoner);
HSTExplanationGenerator multiEx = new HSTExplanationGenerator(explain);
InferredSubClassAxiomGenerator gen = new InferredSubClassAxiomGenerator();
Set<OWLSubClassOfAxiom> subClass = gen.createAxioms(dataFactory, reasoner);
SatisfiabilityConverter converter = new SatisfiabilityConverter(dataFactory);
for (OWLSubClassOfAxiom ax : subClass) {
    System.out.println("\nAxiom :- " + ax);
    System.out.println("Is axiom entailed by reasoner ? :- " + reasoner.isEntailed(ax));
    System.out.println("Is axiom contained in ontology ? :- " + owlOntology.containsAxiom(ax));
    Set<Set<OWLAxiom>> expl = multiEx.getExplanations(converter.convert(ax));
    System.out.println("No. of Explanations :- " + expl.size());
    System.out.println("Explanation :- ");
    for (Set<OWLAxiom> a : expl) {
        System.out.println(a);
    }
}

根据我的代码这里是 output :-

Axiom :- SubClassOf(<http://www.semanticweb.org/ontologies/A#B> owl:Thing)
Is axiom entailed by reasoner ? :- true
Is axiom contained in ontology ? :- false
No. of Explanations :- 1
Explanation :- 
[EquivalentClasses(<http://www.semanticweb.org/ontologies/A#B> <http://www.semanticweb.org/ontologies/A#C> )]

Axiom :- SubClassOf(<http://www.semanticweb.org/ontologies/A#C> owl:Thing)
Is axiom entailed by reasoner ? :- true
Is axiom contained in ontology ? :- false
No. of Explanations :- 1
Explanation :- 
[EquivalentClasses(<http://www.semanticweb.org/ontologies/A#B> <http://www.semanticweb.org/ontologies/A#C> )]

Axiom :- SubClassOf(<http://www.semanticweb.org/ontologies/A#A> <http://www.semanticweb.org/ontologies/A#B>)
Is axiom entailed by reasoner ? :- true
Is axiom contained in ontology ? :- true
No. of Explanations :- 1
Explanation :- 
[SubClassOf(<http://www.semanticweb.org/ontologies/A#A> <http://www.semanticweb.org/ontologies/A#B>)]

Axiom :- SubClassOf(<http://www.semanticweb.org/ontologies/A#A> <http://www.semanticweb.org/ontologies/A#C>)
Is axiom entailed by reasoner ? :- true
Is axiom contained in ontology ? :- false
No. of Explanations :- 1
Explanation :- 
[EquivalentClasses(<http://www.semanticweb.org/ontologies/A#B> <http://www.semanticweb.org/ontologies/A#C> ), SubClassOf(<http://www.semanticweb.org/ontologies/A#A> <http://www.semanticweb.org/ontologies/A#B>)]

我有以下问题：

1) 这段代码足以得到推断的公理吗？（就像我可以检查原始 ontology 中是否有新公理可用，如果没有，那么它是一个推断的公理 - [照顾公理说 C SubClassOf owl:Thing]）

2) reasoner 的 isEntailed() 方法如果总是给出 true 有什么用？

3) 推论公理总有1种解释。这是正确的吗？对于推断公理 A SubClassOf C，有 1 个解释，但它的 Set 与 protege 中显示的相反（顺序）。所以我需要总是反向显示它？

保护图像 :-

Answer 1

1) 是的，这就足够了 - 在 ontology 中包含并存在的公理通常称为 'asserted'。

2) isEntailed() 并不总是 return 正确。它适用于您正在使用的公理 - 如果 owl:Nothing.

尝试询问 owl:Thing 是否是子类

3) 至少有一个蕴含公理的解释。当公理包含在 ontology 中时，它是微不足道的解释 - 所有包含的公理都是蕴含的。对于更复杂的情况，可能有多种解释。

OWLAPI：想要使用 HermiT 推理器从 ontology 中获得推断的公理

OWLAPI : Want to get inferred axioms from ontology using HermiT reasoner

java

ontology

protege

owl-api