informatik/FactProver/FactProver.java

package de.unibremen.informatik.FactProver;

import java.util.Iterator;
import java.util.Set;
import java.util.TreeSet;

import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.IRI;
import org.semanticweb.owlapi.model.OWLAnnotationAssertionAxiom;
import org.semanticweb.owlapi.model.OWLAnnotationAxiom;
import org.semanticweb.owlapi.model.OWLAnnotationPropertyDomainAxiom;
import org.semanticweb.owlapi.model.OWLAnnotationPropertyRangeAxiom;
import org.semanticweb.owlapi.model.OWLAsymmetricObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLClassAssertionAxiom;
import org.semanticweb.owlapi.model.OWLClassAxiom;
import org.semanticweb.owlapi.model.OWLClassExpression;
import org.semanticweb.owlapi.model.OWLDataProperty;
import org.semanticweb.owlapi.model.OWLDataPropertyAssertionAxiom;
import org.semanticweb.owlapi.model.OWLDataPropertyAxiom;
import org.semanticweb.owlapi.model.OWLDataPropertyCharacteristicAxiom;
import org.semanticweb.owlapi.model.OWLDataPropertyDomainAxiom;
import org.semanticweb.owlapi.model.OWLDataPropertyExpression;
import org.semanticweb.owlapi.model.OWLDataPropertyRangeAxiom;
import org.semanticweb.owlapi.model.OWLDatatypeDefinitionAxiom;
import org.semanticweb.owlapi.model.OWLDeclarationAxiom;
import org.semanticweb.owlapi.model.OWLDifferentIndividualsAxiom;
import org.semanticweb.owlapi.model.OWLDisjointClassesAxiom;
import org.semanticweb.owlapi.model.OWLDisjointDataPropertiesAxiom;
import org.semanticweb.owlapi.model.OWLDisjointObjectPropertiesAxiom;
import org.semanticweb.owlapi.model.OWLDisjointUnionAxiom;
import org.semanticweb.owlapi.model.OWLEquivalentClassesAxiom;
import org.semanticweb.owlapi.model.OWLEquivalentDataPropertiesAxiom;
import org.semanticweb.owlapi.model.OWLEquivalentObjectPropertiesAxiom;
import org.semanticweb.owlapi.model.OWLFunctionalDataPropertyAxiom;
import org.semanticweb.owlapi.model.OWLFunctionalObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLIndividual;
import org.semanticweb.owlapi.model.OWLIndividualAxiom;
import org.semanticweb.owlapi.model.OWLInverseFunctionalObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLInverseObjectPropertiesAxiom;
import org.semanticweb.owlapi.model.OWLIrreflexiveObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLLiteral;
import org.semanticweb.owlapi.model.OWLLogicalAxiom;
import org.semanticweb.owlapi.model.OWLNamedIndividual;
import org.semanticweb.owlapi.model.OWLNaryAxiom;
import org.semanticweb.owlapi.model.OWLNaryClassAxiom;
import org.semanticweb.owlapi.model.OWLNaryIndividualAxiom;
import org.semanticweb.owlapi.model.OWLNaryPropertyAxiom;
import org.semanticweb.owlapi.model.OWLNegativeDataPropertyAssertionAxiom;
import org.semanticweb.owlapi.model.OWLNegativeObjectPropertyAssertionAxiom;
import org.semanticweb.owlapi.model.OWLObjectProperty;
import org.semanticweb.owlapi.model.OWLObjectPropertyAssertionAxiom;
import org.semanticweb.owlapi.model.OWLObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLObjectPropertyCharacteristicAxiom;
import org.semanticweb.owlapi.model.OWLObjectPropertyDomainAxiom;
import org.semanticweb.owlapi.model.OWLObjectPropertyExpression;
import org.semanticweb.owlapi.model.OWLObjectPropertyRangeAxiom;
import org.semanticweb.owlapi.model.OWLOntology;
import org.semanticweb.owlapi.model.OWLOntologyCreationException;
import org.semanticweb.owlapi.model.OWLOntologyManager;
import org.semanticweb.owlapi.model.OWLPropertyAssertionAxiom;
import org.semanticweb.owlapi.model.OWLPropertyAxiom;
import org.semanticweb.owlapi.model.OWLPropertyDomainAxiom;
import org.semanticweb.owlapi.model.OWLPropertyRangeAxiom;
import org.semanticweb.owlapi.model.OWLReflexiveObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLSameIndividualAxiom;
import org.semanticweb.owlapi.model.OWLSubAnnotationPropertyOfAxiom;
import org.semanticweb.owlapi.model.OWLSubClassOfAxiom;
import org.semanticweb.owlapi.model.OWLSubDataPropertyOfAxiom;
import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom;
import org.semanticweb.owlapi.model.OWLSubPropertyAxiom;
import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom;
import org.semanticweb.owlapi.model.OWLSymmetricObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom;
import org.semanticweb.owlapi.model.OWLUnaryPropertyAxiom;
import org.semanticweb.owlapi.model.SWRLRule;
import org.semanticweb.owlapi.reasoner.BufferingMode;
import org.semanticweb.owlapi.reasoner.Node;
import org.semanticweb.owlapi.reasoner.NodeSet;
import org.semanticweb.owlapi.reasoner.SimpleConfiguration;

import uk.ac.manchester.cs.factplusplus.FaCTPlusPlusException;
import uk.ac.manchester.cs.factplusplus.owlapiv3.FaCTPlusPlusReasoner;

public class FactProver {
    private IRI iri;
    private FaCTPlusPlusReasoner reasoner;
    private OWLAxiom goal;

    public FactProver(IRI iri)
        throws OWLOntologyCreationException, FaCTPlusPlusException
    {
        this.iri = iri;
        OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
        OWLOntology ontology =
            manager.loadOntologyFromOntologyDocument(this.iri);
        this.reasoner = new FaCTPlusPlusReasoner(ontology,
            new SimpleConfiguration(), BufferingMode.BUFFERING);
    }

    public void loadGoal(IRI giri) throws OWLOntologyCreationException {
        OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
        OWLOntology ontology = manager.loadOntologyFromOntologyDocument(giri);
        Set<OWLAxiom> axioms = ontology.getAxioms();
        for (Iterator<OWLAxiom> i = axioms.iterator(); i.hasNext();) {
            OWLAxiom ax = i.next();
            if (ax instanceof OWLDeclarationAxiom)
                i.remove();
        }
        if (axioms.size() == 1) {
            Iterator<OWLAxiom> it = axioms.iterator();
            this.goal = it.next();
        } else {
            throw new OWLOntologyCreationException("Too many axioms for conjecture");
        }
    }

    public boolean prove() throws FaCTPlusPlusException {
        if (goal instanceof OWLObjectPropertyAssertionAxiom) {
            OWLObjectPropertyAssertionAxiom g =
                (OWLObjectPropertyAssertionAxiom) goal;
            OWLIndividual object = g.getObject();
            OWLIndividual subject = g.getSubject();
            OWLObjectPropertyExpression prop = g.getProperty();
            NodeSet<OWLNamedIndividual> ind = reasoner
                .getObjectPropertyValues(object.asOWLNamedIndividual(), prop);
            return ind.containsEntity(subject.asOWLNamedIndividual());
        }
        if (goal instanceof OWLClassAssertionAxiom) {
            OWLClassAssertionAxiom g = (OWLClassAssertionAxiom) goal;
            OWLClassExpression cls = g.getClassExpression();
            OWLIndividual indi = g.getIndividual();
            NodeSet<OWLClass> n =
                reasoner.getTypes(indi.asOWLNamedIndividual(), true);
            return n.containsEntity(cls.asOWLClass());
        }
        if (goal instanceof OWLDataPropertyAssertionAxiom) {
            OWLDataPropertyAssertionAxiom g =
                (OWLDataPropertyAssertionAxiom) goal;
            OWLDataProperty prop = g.getProperty().asOWLDataProperty();
            OWLLiteral obj = g.getObject();
            OWLIndividual sub = g.getSubject();
            Set<OWLLiteral> litset = reasoner
                .getDataPropertyValues(sub.asOWLNamedIndividual(), prop);
            return litset.contains(obj);
        }
        if (goal instanceof OWLEquivalentClassesAxiom) {
            OWLEquivalentClassesAxiom g = (OWLEquivalentClassesAxiom) goal;
            OWLClassExpression[] cls = g.getClassExpressions()
                .toArray(new OWLClassExpression[g.getClassExpressions().size()]);
            boolean res = true;
            for (int i = 0; i < cls.length; i++ ) {
                for (int j = 0; j < cls.length; j++ ) {
                    if (i != j) {
                        Node<OWLClass> c =
                            reasoner.getEquivalentClasses(cls[i]);
                        res &= c.contains(cls[j].asOWLClass());
                    }
                }
            }
            return res;
        }
        if (goal instanceof OWLSubClassOfAxiom) {
            OWLSubClassOfAxiom g = (OWLSubClassOfAxiom) goal;
            OWLClassExpression sub = g.getSubClass();
            OWLClassExpression top = g.getSuperClass();
            NodeSet<OWLClass> c = reasoner.getSubClasses(top, true);
            return c.containsEntity(sub.asOWLClass());
        }
        if (goal instanceof OWLDataPropertyRangeAxiom) {
            throw new FaCTPlusPlusException("Fact++ cannot determine data ranges!");
        }
        if (goal instanceof OWLDataPropertyDomainAxiom) {
            OWLDataPropertyDomainAxiom g = (OWLDataPropertyDomainAxiom) goal;
            OWLDataProperty prop = g.getProperty().asOWLDataProperty();
            OWLClassExpression d = g.getDomain();
            boolean res = false;
            NodeSet<OWLClass> dom = reasoner.getDataPropertyDomains(prop, true);
            Iterator<Node<OWLClass>> it = dom.iterator();
            while (it.hasNext()) {
                Node<OWLClass> cur = it.next();
                Iterator<OWLClass> itt = cur.iterator();
                while (itt.hasNext()) {
                    OWLClass c = itt.next();
                    Node<OWLClass> cl = reasoner.getEquivalentClasses(c);
                    if (cl.contains(d.asOWLClass()))
                        res = true;
                }
            }
            return res;
        }
        if (goal instanceof OWLSubDataPropertyOfAxiom) {
            OWLSubDataPropertyOfAxiom g = (OWLSubDataPropertyOfAxiom) goal;
            OWLDataProperty sub = g.getSubProperty().asOWLDataProperty();
            OWLDataProperty sup = g.getSuperProperty().asOWLDataProperty();
            boolean res = false;
            NodeSet<OWLDataProperty> sups =
                reasoner.getSuperDataProperties(sub, true);
            Iterator<Node<OWLDataProperty>> it = sups.iterator();
            while (it.hasNext()) {
                Node<OWLDataProperty> cur = it.next();
                if (cur.contains(sup))
                    res = true;
            }
            return res;
        }
        if (goal instanceof OWLAsymmetricObjectPropertyAxiom) {
            throw new FaCTPlusPlusException("Fact++ cannot determine antisymmetry!");
        }
        if (goal instanceof OWLAnnotationAssertionAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLAnnotationAssertionAxiom!");
        }
        if (goal instanceof OWLAnnotationAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLAnnotationAxiom!");
        }
        if (goal instanceof OWLAnnotationPropertyDomainAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLAnnotationPropertyDomainAxiom!");
        }
        if (goal instanceof OWLAnnotationPropertyRangeAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLAnnotationPropertyRangeAxiom!");
        }
        if (goal instanceof OWLClassAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLClassAxiom!");
        }
        if (goal instanceof OWLDataPropertyAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDataPropertyAxiom!");
        }
        if (goal instanceof OWLDataPropertyCharacteristicAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDataPropertyCharacteristicAxiom!");
        }
        if (goal instanceof OWLDatatypeDefinitionAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDatatypeDefinitionAxiom!");
        }
        if (goal instanceof OWLDeclarationAxiom) {
            return true;
        }
        if (goal instanceof OWLDifferentIndividualsAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDifferentIndividualsAxiom!");
        }
        if (goal instanceof OWLDisjointClassesAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDisjointClassesAxiom!");
        }
        if (goal instanceof OWLDisjointDataPropertiesAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDisjointDataPropertiesAxiom!");
        }
        if (goal instanceof OWLDisjointObjectPropertiesAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDisjointObjectPropertiesAxiom!");
        }
        if (goal instanceof OWLDisjointUnionAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLDisjointUnionAxiom!");
        }
        if (goal instanceof OWLIndividualAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLIndividualAxiom!");
        }
        if (goal instanceof OWLLogicalAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLLogicalAxiom!");
        }
        if (goal instanceof OWLNaryAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLNaryAxiom!");
        }
        if (goal instanceof OWLNaryClassAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLNaryClassAxiom!");
        }
        if (goal instanceof OWLNaryIndividualAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLNaryIndividualAxiom!");
        }
        if (goal instanceof OWLNaryPropertyAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLNaryPropertyAxiom!");
        }
        if (goal instanceof OWLObjectPropertyAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLObjectPropertyAxiom!");
        }
        if (goal instanceof OWLObjectPropertyCharacteristicAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLObjectPropertyCharacteristicAxiom!");
        }
        if (goal instanceof OWLPropertyAssertionAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLPropertyAssertionAxiom!");
        }
        if (goal instanceof OWLPropertyAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLPropertyAxiom!");
        }
        if (goal instanceof OWLPropertyDomainAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLPropertyDomainAxiom!");
        }
        if (goal instanceof OWLPropertyRangeAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLPropertyRangeAxiom!");
        }
        if (goal instanceof OWLSameIndividualAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLSameIndividualAxiom!");
        }
        if (goal instanceof OWLSubAnnotationPropertyOfAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLSubAnnotationPropertyOfAxiom!");
        }
        if (goal instanceof OWLSubPropertyAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLSubPropertyAxiom!");
        }
        if (goal instanceof OWLSubPropertyChainOfAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLSubPropertyChainOfAxiom!");
        }
        if (goal instanceof OWLUnaryPropertyAxiom) {
            throw new FaCTPlusPlusException("FaCT++ cannot process OWLUnaryPropertyAxiom!");
        }
        if (goal instanceof SWRLRule) {
            throw new FaCTPlusPlusException("FaCT++ cannot process SWRLRule!");
        }
        if (goal instanceof OWLEquivalentDataPropertiesAxiom) {
            OWLEquivalentDataPropertiesAxiom g =
                (OWLEquivalentDataPropertiesAxiom) goal;
            Set<OWLDataPropertyExpression> props = g.getProperties();
            TreeSet<OWLDataProperty> p = new TreeSet<OWLDataProperty>();
            Iterator<OWLDataPropertyExpression> it = props.iterator();
            p.clear();
            while (it.hasNext()) {
                p.add(it.next().asOWLDataProperty());
            }
            boolean res = true;
            Iterator<OWLDataProperty> itt = p.iterator();
            while (itt.hasNext()) {
                Node<OWLDataProperty> cur =
                    reasoner.getEquivalentDataProperties(itt.next());
                Set<OWLDataProperty> scur = cur.getEntities();
                res &= scur.containsAll(props);
            }
            return res;
        }
        if (goal instanceof OWLEquivalentObjectPropertiesAxiom) {
            OWLEquivalentObjectPropertiesAxiom g =
                (OWLEquivalentObjectPropertiesAxiom) goal;
            Set<OWLObjectPropertyExpression> props = g.getProperties();
            TreeSet<OWLObjectPropertyExpression> p =
                new TreeSet<OWLObjectPropertyExpression>();
            Iterator<OWLObjectPropertyExpression> it = props.iterator();
            p.clear();
            while (it.hasNext()) {
                p.add(it.next());
            }
            boolean res = true;
            Iterator<OWLObjectPropertyExpression> itt = p.iterator();
            while (itt.hasNext()) {
                Node<OWLObjectPropertyExpression> cur =
                    reasoner.getEquivalentObjectProperties(itt.next());
                Set<OWLObjectPropertyExpression> scur = cur.getEntities();
                res &= scur.containsAll(props);
            }
            return res;
        }
        if (goal instanceof OWLFunctionalDataPropertyAxiom) {
            OWLFunctionalDataPropertyAxiom g =
                (OWLFunctionalDataPropertyAxiom) goal;
            OWLDataProperty prop = g.getProperty().asOWLDataProperty();
            return prop.isFunctional(reasoner.getRootOntology());
        }
        if (goal instanceof OWLFunctionalObjectPropertyAxiom) {
            OWLFunctionalObjectPropertyAxiom g =
                (OWLFunctionalObjectPropertyAxiom) goal;
            OWLObjectProperty prop = g.getProperty().asOWLObjectProperty();
            return prop.isFunctional(reasoner.getRootOntology());
        }
        if (goal instanceof OWLInverseFunctionalObjectPropertyAxiom) {
            OWLInverseFunctionalObjectPropertyAxiom g =
                (OWLInverseFunctionalObjectPropertyAxiom) goal;
            OWLObjectProperty prop = g.getProperty().asOWLObjectProperty();
            return prop.isInverseFunctional(reasoner.getRootOntology());
        }
        if (goal instanceof OWLInverseObjectPropertiesAxiom) {
            OWLInverseObjectPropertiesAxiom g =
                (OWLInverseObjectPropertiesAxiom) goal;
            OWLObjectPropertyExpression fst = g.getFirstProperty();
            OWLObjectPropertyExpression snd = g.getSecondProperty();
            Node<OWLObjectPropertyExpression> is =
                reasoner.getInverseObjectProperties(fst);
            boolean res = false;
            if (is.contains(snd)) {
                res = true;
            }
            return res;
        }
        if (goal instanceof OWLIrreflexiveObjectPropertyAxiom) {
            OWLIrreflexiveObjectPropertyAxiom g =
                (OWLIrreflexiveObjectPropertyAxiom) goal;
            return g.getProperty().asOWLObjectProperty()
                .isIrreflexive(reasoner.getRootOntology());
        }
        if (goal instanceof OWLNegativeDataPropertyAssertionAxiom) {
            OWLNegativeDataPropertyAssertionAxiom g =
                (OWLNegativeDataPropertyAssertionAxiom) goal;
            OWLIndividual sub = g.getSubject();
            OWLLiteral obj = g.getObject();
            OWLDataProperty p = g.getProperty().asOWLDataProperty();
            Set<OWLLiteral> slit =
                reasoner.getDataPropertyValues(sub.asOWLNamedIndividual(), p);
            return slit.contains(obj);
        }
        if (goal instanceof OWLNegativeObjectPropertyAssertionAxiom) {
            OWLNegativeObjectPropertyAssertionAxiom g =
                (OWLNegativeObjectPropertyAssertionAxiom) goal;
            OWLIndividual sub = g.getSubject();
            OWLIndividual obj = g.getObject();
            OWLObjectProperty p = g.getProperty().asOWLObjectProperty();
            NodeSet<OWLNamedIndividual> ind =
                reasoner.getObjectPropertyValues(obj.asOWLNamedIndividual(), p);
            return ind.containsEntity(sub.asOWLNamedIndividual());
        }
        if (goal instanceof OWLObjectPropertyAssertionAxiom) {
            OWLObjectPropertyAssertionAxiom g =
                (OWLObjectPropertyAssertionAxiom) goal;
            OWLIndividual sub = g.getSubject();
            OWLIndividual obj = g.getObject();
            OWLObjectProperty p = g.getProperty().asOWLObjectProperty();
            NodeSet<OWLNamedIndividual> ind =
                reasoner.getObjectPropertyValues(obj.asOWLNamedIndividual(), p);
            return ind.containsEntity(sub.asOWLNamedIndividual());
        }
        if (goal instanceof OWLObjectPropertyDomainAxiom) {
            OWLObjectPropertyDomainAxiom g =
                (OWLObjectPropertyDomainAxiom) goal;
            OWLObjectPropertyExpression prop = g.getProperty();
            OWLClassExpression dom = g.getDomain();
            NodeSet<OWLClass> doms =
                reasoner.getObjectPropertyDomains(prop, true);
            boolean res = false;
            Iterator<Node<OWLClass>> it = doms.iterator();
            while (it.hasNext()) {
                Node<OWLClass> cur = it.next();
                if (cur.contains(dom.asOWLClass())) {
                    res = true;
                }
            }
            return res;
        }
        if (goal instanceof OWLObjectPropertyRangeAxiom) {
            OWLObjectPropertyRangeAxiom g = (OWLObjectPropertyRangeAxiom) goal;
            OWLObjectPropertyExpression prop = g.getProperty();
            OWLClass ran = g.getRange().asOWLClass();
            NodeSet<OWLClass> rns =
                reasoner.getObjectPropertyRanges(prop, true);
            return rns.containsEntity(ran);
        }
        if (goal instanceof OWLSubObjectPropertyOfAxiom) {
            OWLSubObjectPropertyOfAxiom g = (OWLSubObjectPropertyOfAxiom) goal;
            OWLObjectPropertyExpression sub = g.getSubProperty();
            OWLObjectPropertyExpression sup = g.getSuperProperty();
            NodeSet<OWLObjectPropertyExpression> subs =
                reasoner.getSubObjectProperties(sup, true);
            boolean res = false;
            Iterator<Node<OWLObjectPropertyExpression>> it = subs.iterator();
            while (it.hasNext()) {
                Node<OWLObjectPropertyExpression> cur = it.next();
                if (cur.contains(sub)) {
                    res = true;
                }
            }
            return res;
        }
        if (goal instanceof OWLReflexiveObjectPropertyAxiom) {
            OWLReflexiveObjectPropertyAxiom g =
                (OWLReflexiveObjectPropertyAxiom) goal;
            OWLObjectProperty prop = g.getProperty().asOWLObjectProperty();
            return prop.isReflexive(reasoner.getRootOntology());
        }
        if (goal instanceof OWLSymmetricObjectPropertyAxiom) {
            OWLSymmetricObjectPropertyAxiom g =
                (OWLSymmetricObjectPropertyAxiom) goal;
            OWLObjectProperty prop = g.getProperty().asOWLObjectProperty();
            return prop.isSymmetric(reasoner.getRootOntology());
        }
        if (goal instanceof OWLTransitiveObjectPropertyAxiom) {
            OWLTransitiveObjectPropertyAxiom g =
                (OWLTransitiveObjectPropertyAxiom) goal;
            OWLObjectProperty prop = g.getProperty().asOWLObjectProperty();
            return prop.isTransitive(reasoner.getRootOntology());
        }
        System.out.println(goal);
        throw new FaCTPlusPlusException("No reasoner found, sorry!");
    }
}