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