Prove.java revision b3801e7f361759d6748a661df75c01c084299c67
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiupackage de.unibremen.informatik.FactProver;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiuimport java.net.URI;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiuimport org.semanticweb.owlapi.model.IRI;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiupublic class Prove {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu public static void main (String[] args)
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu if (args.length < 2)
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.out.println("owl_fact_prover <Ontology> <Conjecture>");
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.exit(1);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu }
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu try
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu IRI physicalIRI = IRI.create(args[0]);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu IRI goalIRI = IRI.create(args[1]);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu FactProver prover = new FactProver(physicalIRI);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu prover.loadGoal(goalIRI);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu boolean res = prover.prove();
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu if (res)
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.out.println("proved");
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.exit(10);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu }
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu else
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.out.println("disproved");
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.exit(20);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu }
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu }
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu catch (Exception e)
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu {
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.out.println(e.getMessage());
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu System.exit(1);
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu }
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu }
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu}