How to perform existential quantification inferences in ontologies?

Question

I'm attempting to compute existential quantification inferences in an ontology, as exemplified below. Given the ontology:

Politician(Albert)
Politician(Bob)
related(Albert, Bob)

I would like to have the following inference:

∃ related.Politician

I tried to do this by using ELK and HermiT reasoners in an OWLAPI application and also through Protégé. However, it seems that these reasoners are not computing this specific type of inferences.

Here is a snippet of my code:

    /**
     * Compute the ontology along with the inferred consequences
     * @throws OWLOntologyCreationException
     */
    public void computeInferredOntology() throws OWLOntologyCreationException {
        logger.info("Computing inferences...");

        reasoner.precomputeInferences();

        logger.info("Creating axiom generators list...");

        // To generate an inferred ontology we use implementations of inferred axiom generators
        List<InferredAxiomGenerator<? extends OWLAxiom>> generators = new ArrayList<InferredAxiomGenerator<? extends OWLAxiom>>();
        generators.add(new InferredClassAssertionAxiomGenerator());
        generators.add(new InferredSubClassAxiomGenerator());
        generators.add(new InferredEquivalentClassAxiomGenerator());
        generators.add(new InferredEquivalentDataPropertiesAxiomGenerator());
        generators.add(new InferredEquivalentObjectPropertyAxiomGenerator());
        generators.add(new InferredDataPropertyCharacteristicAxiomGenerator());
        generators.add(new InferredSubDataPropertyAxiomGenerator());
        generators.add(new InferredSubObjectPropertyAxiomGenerator());
        // generators.add(new InferredDisjointClassesAxiomGenerator());
        // generators.add(new InferredPropertyAssertionGenerator());

        logger.info("Generating inferred ontology...");

        // Put the inferred axioms into a fresh empty ontology.
        inferredOntology = ontologyManager.createOntology();
        ontologyManager.addAxioms(inferredOntology, ontology.getAxioms());
        InferredOntologyGenerator inferredOntologyGenerator = new InferredOntologyGenerator(reasoner, generators);
        inferredOntologyGenerator.fillOntology(ontologyManager.getOWLDataFactory(), inferredOntology);
    }

I would like to know if there is any reasoner that can handle this kind of inferences. Also, is this a known problem with some specific algorithms?

Thank you all.

Answer 1

Both Hermit and Elk support existential quantifiers. The problem is how you think this works, is different from how it actually works, both from an OWL and description logic perspective.

There is at least 2 reasons why no reasoner will make the inference you expect:

1. Reasoners only make inferences in terms of known classes. ∃related.Politician is a class expression or anonymous class - that is it describes a class without giving it a name. In your example Politician is a class. Reasoners restrict inferences to known classes otherwise the number of inferences are infinite.

2. Description logic/OWL reasoners make 3 specific types of inferences which are:

(a) classification, i.e., Politician SubClassOf Person, assuming the ontology has a Person class and related axioms to make this inference.

(b) instance checking, i.e., the individual bob is an instance of Politician.

(c) satisfiability checking, i.e., checking that the class Politician is not forced to be empty. A class is forced to be empty if there is a logical inconsistency in the ontology. An example if we define Politician EquivalentTo Person and not Person, then the Politician class is unsatisfiable.

Note that your inference is not in this list and as such it cannot be derived by a reasoner.

I write about ontologies and reasoning on my blog and in particular existential restrictions here. I also explain the semantics of description logics which helps one understand the inferences that follow from a reasoner here. I assume the audience have no knowledge of logic.