Permalink
Browse files

Adapt to changes in the Proof interface of puli

+ some resulting simplifications
  • Loading branch information...
ykazakov committed Oct 6, 2017
1 parent 7cf796d commit 934a9657c5cac9ed225b562cbcd321c1407f536e
Showing with 414 additions and 419 deletions.
  1. +10 −9 ...distribution/src/main/java/org/semanticweb/elk/owlapi/examples/RetrievingProofsForEntailment.java
  2. +2 −1 elk-owlapi/src/main/java/org/semanticweb/elk/owlapi/ElkProver.java
  3. +8 −8 elk-owlapi/src/main/java/org/semanticweb/elk/owlapi/proofs/ElkOwlProof.java
  4. +57 −0 elk-owlapi/src/main/java/org/semanticweb/elk/owlapi/proofs/OwlInternalJustifier.java
  5. +1 −21 elk-owlapi/src/main/java/org/semanticweb/elk/owlapi/proofs/OwlInternalProof.java
  6. +16 −6 elk-owlapi/src/test/java/org/semanticweb/elk/owlapi/proofs/OwlInternalProofTest.java
  7. +3 −1 elk-owlapi/src/test/java/org/semanticweb/elk/owlapi/proofs/ProofTest.java
  8. +15 −12 elk-owlapi/src/test/java/org/semanticweb/elk/owlapi/proofs/ProofTestUtils.java
  9. +1 −2 elk-proofs/src/main/java/org/semanticweb/elk/owl/inferences/ElkProof.java
  10. +4 −4 elk-proofs/src/main/java/org/semanticweb/elk/owl/inferences/ElkProofGenerator.java
  11. +1 −2 elk-proofs/src/main/java/org/semanticweb/elk/owl/inferences/ModifiableElkProof.java
  12. +6 −5 elk-proofs/src/main/java/org/semanticweb/elk/owl/inferences/ReasonerElkProof.java
  13. +78 −0 elk-proofs/src/main/java/org/semanticweb/elk/proofs/InternalJustifier.java
  14. +7 −83 elk-proofs/src/main/java/org/semanticweb/elk/proofs/InternalProof.java
  15. +57 −0 elk-proofs/src/main/java/org/semanticweb/elk/proofs/TracingInferenceWrap.java
  16. +1 −1 elk-proofs/src/test/java/org/semanticweb/elk/owl/inferences/TestUtils.java
  17. +17 −4 ...protege/src/main/java/org/semanticweb/elk/protege/proof/ElkInternalJustificationProofService.java
  18. +3 −2 elk-protege/src/main/java/org/semanticweb/elk/protege/proof/ElkJustificationProofService.java
  19. +2 −2 elk-protege/src/main/java/org/semanticweb/elk/protege/proof/ElkOwlInferenceExamples.java
  20. +16 −53 elk-protege/src/main/java/org/semanticweb/elk/protege/proof/ElkOwlJustificationProofService.java
  21. +9 −7 elk-protege/src/main/java/org/semanticweb/elk/protege/proof/ElkProofService.java
  22. +0 −37 elk-protege/src/main/java/org/semanticweb/elk/protege/proof/JustificationCompleteInternalProof.java
  23. +13 −13 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/consistency/ConsistencyCheckingState.java
  24. +0 −44 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/entailments/EntailmentProofUnion.java
  25. +10 −6 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/entailments/InconsistencyProofWrapper.java
  26. +1 −1 ...asoner/src/main/java/org/semanticweb/elk/reasoner/entailments/model/AxiomEntailmentInference.java
  27. +1 −1 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/entailments/model/EntailmentInference.java
  28. +0 −29 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/entailments/model/EntailmentProof.java
  29. +10 −9 ...easoner/src/main/java/org/semanticweb/elk/reasoner/query/AbstractEntailmentQueryWithPremises.java
  30. +4 −5 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/query/ClassAssertionEntailmentQuery.java
  31. +4 −3 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/query/IndexedEntailmentQuery.java
  32. +4 −5 ...oner/src/main/java/org/semanticweb/elk/reasoner/query/ObjectPropertyAssertionEntailmentQuery.java
  33. +4 −5 ...easoner/src/main/java/org/semanticweb/elk/reasoner/query/ObjectPropertyDomainEntailmentQuery.java
  34. +4 −2 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/query/ProperEntailmentQueryResult.java
  35. +4 −5 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/query/SubClassOfEntailmentQuery.java
  36. +6 −4 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/stages/AbstractReasonerState.java
  37. +9 −10 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/stages/EntailmentQueryState.java
  38. +3 −3 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/tracing/GenericTracingProof.java
  39. +1 −1 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/tracing/ModifiableTracingProof.java
  40. +13 −8 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/tracing/ModifiableTracingProofImpl.java
  41. +1 −1 ...asoner/src/main/java/org/semanticweb/elk/reasoner/tracing/SynchronizedModifiableTracingProof.java
  42. +6 −2 elk-reasoner/src/main/java/org/semanticweb/elk/reasoner/tracing/TraceState.java
  43. +2 −2 elk-reasoner/src/test/java/org/semanticweb/elk/reasoner/tracing/TracingTestUtils.java
@@ -31,6 +31,7 @@
import java.util.Set;
import org.liveontologies.owlapi.proof.OWLProver;
import org.liveontologies.puli.DynamicProof;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.Proof;
import org.semanticweb.elk.owlapi.ElkProverFactory;
@@ -74,34 +75,34 @@ public static void main(String[] args) throws OWLOntologyCreationException {
OWLAxiom entailment = getEntailment();
// Get the inferences used to prove the entailment
Proof<OWLAxiom> inferences = prover.getProof(entailment);
DynamicProof<? extends Inference<OWLAxiom>> proof = prover.getProof(entailment);
// Now we can recursively request inferences and their premises. Print them to std.out in this example.
unwindProofs(inferences, entailment);
unwindProof(proof, entailment);
// Terminate the worker threads used by the reasoner.
prover.dispose();
}
private static <C> void unwindProofs(Proof<C> inferences, C entailment) {
// Start recursive unwinding
LinkedList<C> toDo = new LinkedList<C>();
Set<C> done = new HashSet<C>();
private static void unwindProof(Proof<?> proof, Object entailment) {
// Start recursive unwinding of conclusions
LinkedList<Object> toDo = new LinkedList<Object>();
Set<Object> done = new HashSet<Object>();
toDo.add(entailment);
done.add(entailment);
for (;;) {
C next = toDo.poll();
Object next = toDo.poll();
if (next == null) {
break;
}
for (Inference<C> inf : inferences.getInferences(next)) {
for (Inference<?> inf : proof.getInferences(next)) {
System.out.println(inf);
// Recursively unwind premise inferences
for (C premise : inf.getPremises()) {
for (Object premise : inf.getPremises()) {
if (done.add(premise)) {
toDo.addFirst(premise);
@@ -23,6 +23,7 @@
import org.liveontologies.owlapi.proof.OWLProver;
import org.liveontologies.puli.DynamicProof;
import org.semanticweb.elk.owlapi.proofs.ElkOwlInference;
import org.semanticweb.elk.owlapi.proofs.ElkOwlProof;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.reasoner.UnsupportedEntailmentTypeException;
@@ -35,7 +36,7 @@ public ElkProver(ElkReasoner elkReasoner) {
}
@Override
public DynamicProof<OWLAxiom> getProof(OWLAxiom entailment)
public DynamicProof<ElkOwlInference> getProof(OWLAxiom entailment)
throws UnsupportedEntailmentTypeException {
return ElkOwlProof.create(getDelegate(), entailment);
}
@@ -24,7 +24,8 @@
import java.util.Collection;
import org.liveontologies.puli.BaseProof;
import org.liveontologies.puli.GenericDynamicProof;
import org.liveontologies.puli.DynamicProof;
import org.liveontologies.puli.Proof;
import org.liveontologies.puli.Proofs;
import org.semanticweb.elk.exceptions.ElkException;
import org.semanticweb.elk.exceptions.ElkRuntimeException;
@@ -36,15 +37,15 @@
import org.semanticweb.elk.owlapi.ElkConverter;
import org.semanticweb.elk.owlapi.ElkReasoner;
import org.semanticweb.elk.owlapi.wrapper.OwlConverter;
import org.semanticweb.elk.reasoner.entailments.model.EntailmentProof;
import org.semanticweb.elk.reasoner.entailments.model.EntailmentInference;
import org.semanticweb.elk.reasoner.query.EntailmentQueryResult;
import org.semanticweb.elk.reasoner.query.ProperEntailmentQueryResult;
import org.semanticweb.elk.reasoner.query.UnsupportedIndexingEntailmentQueryResult;
import org.semanticweb.elk.reasoner.query.UnsupportedQueryTypeEntailmentQueryResult;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.reasoner.UnsupportedEntailmentTypeException;
public class ElkOwlProof extends BaseProof<OWLAxiom, ElkOwlInference>
public class ElkOwlProof extends BaseProof<ElkOwlInference>
implements ElkReasoner.ChangeListener {
private final ElkReasoner elkReasoner_;
@@ -70,7 +71,7 @@ private ElkOwlProof(ElkReasoner elkReasoner, OWLAxiom elkEntailment) {
@Override
public synchronized Collection<? extends ElkOwlInference> getInferences(
OWLAxiom conclusion) {
Object conclusion) {
ensureSync();
return super.getInferences(conclusion);
}
@@ -123,7 +124,7 @@ public Void visit(final ProperEntailmentQueryResult properResult)
ElkOwlProof.this);
final ElkInference.Factory factory = new ElkInferenceOptimizedProducingFactory(
producer);
final EntailmentProof evidence = properResult
final Proof<EntailmentInference> evidence = properResult
.getEvidence(false);
new ElkProofGenerator(evidence,
elkReasoner_.getInternalReasoner(), factory)
@@ -153,9 +154,8 @@ public Void visit(
};
public static GenericDynamicProof<OWLAxiom, ElkOwlInference> create(
ElkReasoner reasoner, OWLAxiom entailment)
throws UnsupportedEntailmentTypeException {
public static DynamicProof<ElkOwlInference> create(ElkReasoner reasoner,
OWLAxiom entailment) throws UnsupportedEntailmentTypeException {
if (reasoner == null) {
return Proofs.emptyProof();
}
@@ -0,0 +1,57 @@
package org.semanticweb.elk.owlapi.proofs;
/*-
* #%L
* ELK OWL API Binding
* $Id:$
* $HeadURL:$
* %%
* Copyright (C) 2011 - 2017 Department of Computer Science, University of Oxford
* %%
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
* #L%
*/
import java.util.Set;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.InferenceJustifier;
import org.semanticweb.elk.owl.interfaces.ElkAxiom;
import org.semanticweb.elk.owlapi.ElkConverter;
import org.semanticweb.elk.proofs.InternalJustifier;
import org.semanticweb.owlapi.model.OWLAxiom;
import com.google.common.base.Function;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Iterables;
public class OwlInternalJustifier
implements InferenceJustifier<Inference<?>, Set<OWLAxiom>>,
Function<ElkAxiom, OWLAxiom> {
private final InferenceJustifier<Inference<?>, Set<? extends ElkAxiom>> internalJustifier_ = new InternalJustifier();
private final ElkConverter elkConverter_ = ElkConverter.getInstance();
@Override
public Set<OWLAxiom> getJustification(Inference<?> inference) {
return ImmutableSet.copyOf(Iterables.transform(
internalJustifier_.getJustification(inference), this));
}
@Override
public OWLAxiom apply(final ElkAxiom input) {
return elkConverter_.convert(input);
}
}
@@ -23,11 +23,8 @@
import java.util.Arrays;
import java.util.Collection;
import java.util.Set;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.InferenceJustifier;
import org.liveontologies.puli.InferenceJustifiers;
import org.liveontologies.puli.Inferences;
import org.liveontologies.puli.Proof;
import org.semanticweb.elk.exceptions.ElkException;
@@ -41,18 +38,14 @@
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.reasoner.UnsupportedEntailmentTypeException;
import com.google.common.base.Function;
public class OwlInternalProof implements Proof<Object>,
InferenceJustifier<Object, Set<? extends OWLAxiom>> {
public class OwlInternalProof implements Proof<Inference<Object>> {
private final OwlConverter owlConverter_ = OwlConverter.getInstance();
private final ElkConverter elkConverter_ = ElkConverter.getInstance();
private final OWLAxiom goal_;
private final Inference<Object> goalInference_;
private final InternalProofExtension proof_;
private final InferenceJustifier<Object, ? extends Set<? extends OWLAxiom>> justifier_;
public OwlInternalProof(final Reasoner reasoner, final OWLAxiom goal) {
this.goal_ = goal;
@@ -62,13 +55,6 @@ public OwlInternalProof(final Reasoner reasoner, final OWLAxiom goal) {
try {
this.proof_ = new InternalProofExtension(reasoner,
owlConverter_.convert(goal));
this.justifier_ = InferenceJustifiers.transform(proof_,
new Function<ElkAxiom, OWLAxiom>() {
@Override
public OWLAxiom apply(final ElkAxiom input) {
return elkConverter_.convert(input);
}
});
} catch (final ElkException e) {
throw elkConverter_.convert(e);
} catch (final ElkRuntimeException e) {
@@ -93,12 +79,6 @@ public Object getGoal() {
return proof_.getInferences(conclusion);
}
@Override
public Set<? extends OWLAxiom> getJustification(
Inference<Object> inference) {
return justifier_.getJustification(inference);
}
private class InternalProofExtension extends InternalProof {
public InternalProofExtension(final Reasoner reasoner,
@@ -52,12 +52,22 @@
// @formatter:off
static final String[] IGNORE_LIST = {
ElkTestUtils.TEST_INPUT_LOCATION + "/query/entailment/AssertionRanges.owl",// Ranges not supported with assertions
ElkTestUtils.TEST_INPUT_LOCATION + "/query/entailment/HasValueRanges.owl",// Ranges not supported with ObjectHasValue
};
ElkTestUtils.TEST_INPUT_LOCATION
+ "/query/entailment/AssertionRanges.owl", // Ranges not
// supported
// with
// assertions
ElkTestUtils.TEST_INPUT_LOCATION
+ "/query/entailment/HasValueRanges.owl",// Ranges not
// supported
// with
// ObjectHasValue
};
static final String[] IGNORE_COMPLETENESS_LIST = {
ElkTestUtils.TEST_INPUT_LOCATION + "/query/entailment/EmptyOntology.owl",// All entailments are tautologies.
};
ElkTestUtils.TEST_INPUT_LOCATION
+ "/query/entailment/EmptyOntology.owl",// All entailments
// are tautologies.
};
// @formatter:on
static {
@@ -103,7 +113,7 @@ public void testProofCompleteness() throws Exception {
Assume.assumeFalse(TestUtils.ignore(manifest_.getInput(),
ElkTestUtils.TEST_INPUT_LOCATION, IGNORE_COMPLETENESS_LIST));
ProofTestUtils.proofCompletenessTest(prover_, query_,
adapter_.getGoal(), adapter_, adapter_, true);
adapter_.getGoal(), adapter_, new OwlInternalJustifier(), true);
}
@Config
@@ -34,6 +34,7 @@
import org.junit.Test;
import org.liveontologies.owlapi.proof.OWLProver;
import org.liveontologies.puli.DynamicProof;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.ProofNode;
import org.liveontologies.puli.ProofNodes;
import org.liveontologies.puli.ProofStep;
@@ -388,7 +389,8 @@ public void proofListener() throws Exception {
final OWLProver prover = OWLAPITestUtils.createProver(
OWLAPITestUtils.createReasoner(ontology, bufferringMode));
OWLSubClassOfAxiom entailment = factory.getOWLSubClassOfAxiom(a, b);
DynamicProof<OWLAxiom> proof = prover.getProof(entailment);
DynamicProof<? extends Inference<OWLAxiom>> proof = prover
.getProof(entailment);
ProofChangeTracker tracker = new ProofChangeTracker();
proof.addListener(tracker);
@@ -32,6 +32,7 @@
import java.util.Set;
import org.liveontologies.owlapi.proof.OWLProver;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.InferenceJustifier;
import org.liveontologies.puli.InferenceJustifiers;
import org.liveontologies.puli.Proof;
@@ -66,14 +67,14 @@
*/
public class ProofTestUtils {
public static <C> void provabilityTest(final Proof<C> proof,
final C conclusion) {
public static void provabilityTest(final Proof<?> proof,
final Object conclusion) {
assertTrue(String.format("Conclusion %s not derivable!", conclusion),
isDerivable(proof, conclusion));
}
public static <C> boolean isDerivable(final Proof<C> proof,
final C conclusion) {
public static boolean isDerivable(final Proof<?> proof,
final Object conclusion) {
return Proofs.isDerivable(proof, conclusion);
}
@@ -163,25 +164,27 @@ public static void proofCompletenessTest(final OWLProver prover,
public static void proofCompletenessTest(final OWLProver prover,
final OWLAxiom conclusion, final boolean mustNotBeATautology) {
final OWLOntology ontology = prover.getRootOntology();
final Proof<OWLAxiom> proof = Proofs.addAssertedInferences(
Proof<Inference<OWLAxiom>> proof = Proofs.removeAssertedInferences(
prover.getProof(conclusion),
ontology.getAxioms(Imports.INCLUDED));
final InferenceJustifier<OWLAxiom, ? extends Set<? extends OWLAxiom>> justifier = InferenceJustifiers
final InferenceJustifier<Inference<OWLAxiom>, ? extends Set<? extends OWLAxiom>> justifier = InferenceJustifiers
.justifyAssertedInferences();
proofCompletenessTest(prover, conclusion, conclusion, proof, justifier,
mustNotBeATautology);
}
public static <C> void proofCompletenessTest(final OWLProver prover,
final OWLAxiom entailment, final C conclusion, final Proof<C> proof,
final InferenceJustifier<C, ? extends Set<? extends OWLAxiom>> justifier) {
public static <I extends Inference<?>> void proofCompletenessTest(
final OWLProver prover, final OWLAxiom entailment,
final Object conclusion, final Proof<? extends I> proof,
final InferenceJustifier<? super I, ? extends Set<? extends OWLAxiom>> justifier) {
proofCompletenessTest(prover, entailment, conclusion, proof, justifier,
false);
}
public static <C> void proofCompletenessTest(final OWLProver prover,
final OWLAxiom entailment, final C conclusion, final Proof<C> proof,
final InferenceJustifier<C, ? extends Set<? extends OWLAxiom>> justifier,
public static <I extends Inference<?>> void proofCompletenessTest(
final OWLProver prover, final OWLAxiom entailment,
final Object conclusion, final Proof<? extends I> proof,
final InferenceJustifier<? super I, ? extends Set<? extends OWLAxiom>> justifier,
final boolean mustNotBeATautology) {
final OWLOntology ontology = prover.getRootOntology();
@@ -22,8 +22,7 @@
package org.semanticweb.elk.owl.inferences;
import org.liveontologies.puli.Proof;
import org.semanticweb.elk.owl.interfaces.ElkAxiom;
public interface ElkProof extends Proof<ElkAxiom> {
public interface ElkProof extends Proof<ElkInference> {
}
Oops, something went wrong.

0 comments on commit 934a965

Please sign in to comment.