FactProver.java revision e2f328730bd39975b02329b81b608d23193f1c3a
public class FactProver
{
private FaCTPlusPlusReasoner reasoner;
{
this.reasoner = new FaCTPlusPlusReasoner(ontology,new SimpleConfiguration(),BufferingMode.BUFFERING);
}
{
if (ax instanceof OWLDeclarationAxiom)
i.remove();
}
{
}
else
{
throw new OWLOntologyCreationException
("Too many axioms for conjecture");
}
}
public boolean prove() throws FaCTPlusPlusException
{
if (goal instanceof OWLObjectPropertyAssertionAxiom)
{
NodeSet<OWLNamedIndividual> ind = reasoner.getObjectPropertyValues (object.asOWLNamedIndividual(),prop);
}
if (goal instanceof OWLClassAssertionAxiom)
{
}
if (goal instanceof OWLDataPropertyAssertionAxiom)
{
}
if (goal instanceof OWLEquivalentClassesAxiom)
{
boolean res = true;
{
{
if (i != j)
{
}
}
}
return res;
}
if (goal instanceof OWLSubClassOfAxiom)
{
}
if (goal instanceof OWLDataPropertyRangeAxiom)
{
throw new FaCTPlusPlusException
("Fact++ cannot determine data ranges!");
}
if (goal instanceof OWLDataPropertyDomainAxiom)
{
OWLClassExpression d = g.getDomain();
boolean res = false;
res = true;
}
}
return res;
}
if (goal instanceof OWLSubDataPropertyOfAxiom)
{
boolean res = false;
{
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!");
}
{
throw new FaCTPlusPlusException
("FaCT++ cannot process SWRLRule!");
}
if (goal instanceof OWLEquivalentDataPropertiesAxiom)
{
p.clear();
{
}
boolean res = true;
{
}
return res;
}
if (goal instanceof OWLEquivalentObjectPropertiesAxiom)
{
p.clear();
{
}
boolean res = true;
{
}
return res;
}
if (goal instanceof OWLFunctionalDataPropertyAxiom)
{
}
if (goal instanceof OWLFunctionalObjectPropertyAxiom)
{
}
if (goal instanceof OWLInverseFunctionalObjectPropertyAxiom)
{
}
if (goal instanceof OWLInverseObjectPropertiesAxiom)
{
boolean res = false;
return res;
}
if (goal instanceof OWLIrreflexiveObjectPropertyAxiom)
{
}
if (goal instanceof OWLNegativeDataPropertyAssertionAxiom)
{
}
if (goal instanceof OWLNegativeObjectPropertyAssertionAxiom)
{
}
if (goal instanceof OWLObjectPropertyAssertionAxiom)
{
}
if (goal instanceof OWLObjectPropertyDomainAxiom)
{
boolean res = false;
{
}
return res;
}
if (goal instanceof OWLObjectPropertyRangeAxiom)
{
}
if (goal instanceof OWLSubObjectPropertyOfAxiom)
{
boolean res = false;
{
}
return res;
}
if (goal instanceof OWLReflexiveObjectPropertyAxiom)
{
}
if (goal instanceof OWLSymmetricObjectPropertyAxiom)
{
}
if (goal instanceof OWLTransitiveObjectPropertyAxiom)
{
}
throw new FaCTPlusPlusException
("No reasoner found, sorry!");
}
}