/*-
 * #%L
 * OWL API Proof Extension
 * $Id:$
 * $HeadURL:$
 * %%
 * Copyright (C) 2014 - 2016 Live Ontologies Project
 * %%
 * 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%
 */
package org.liveontologies.owlapi.proof;

import org.liveontologies.puli.DynamicProof;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.Inferences;
import org.liveontologies.puli.Proof;
import org.liveontologies.puli.Proofs;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.reasoner.OWLReasoner;
import org.semanticweb.owlapi.reasoner.UnsupportedEntailmentTypeException;

/**
 * An {@link OWLReasoner} that can provide proofs for the entailed axioms.
 * 
 * @author Pavel Klinov
 * 
 *         pavel.klinov@uni-ulm.de
 * 
 * @author Yevgeny Kazakov
 */
public interface OWLProver extends OWLReasoner {

	/**
	 * @param entailment
	 * @return the inferences using which the entailment can be derived from the
	 *         axioms in the ontology. The inferences deriving the axioms in the
	 *         ontology can be tested using
	 *         {@link Inferences#isAsserted(Inference)} and removed from the
	 *         proof using {@link Proofs#removeAssertedInferences(Proof)}.
	 * @throws UnsupportedEntailmentTypeException
	 *             if the proof cannot be provided for the given entailment type
	 */
	public DynamicProof<? extends Inference<OWLAxiom>> getProof(OWLAxiom entailment)
			throws UnsupportedEntailmentTypeException;

}

@@ -864,46 +864,8 @@
 es;%0A
-import org.liveontologies.puli.Proof;%0A
 impo
@@ -1339,64 +1339,153 @@
 %09 * 
-@return the inferences using which the entailment can be
+           the %7B@link OWLAxiom%7D which needs to be proved%0A%09 * %0A%09 * @return the %7B@link DynamicProof%7D using which the given axiom can be%0A%09 *        
  der
@@ -1497,28 +1497,16 @@
 from the
-%0A%09 *        
  axioms 
@@ -1524,238 +1524,697 @@
 logy
-. The inferences
+, if it is entailed. If%0A%09 *         the axiom is not entailed, any proof that does not
  deriv
-ing
+e
  the
- axioms in the%0A%09 *         ontology can be tested using%0A%09 *         %7B@link Inferences#isAsserted(Inference)%7D and removed from the%0A%09 *         proof using %7B@link Proofs#removeAss
+%0A%09 *         given axiom can be returned, e.g., the empty proof.%0A%09 * %0A%09 *         For deriving axioms that occur in the ontology, the proof should%0A%09 *         use asserted inferences (for which%0A%09 *         %7B@link Inferences#isAsserted(Inference)%7D returns %7B@code true%7D).%0A%09 * %0A%09 *         If the proof for the given axiom changes (i.e., the result of%0A%09 *         calling this method with the same axiom would be come different,%0A%09 *         e.g., due to the changes in the ontology), the regist
 er
-t
 ed
-Inferences(Proof)%7D.
+%0A%09 *         listeners of the %7B@link DynamicProof%7D must be notified%0A%09 *         accordingly.%0A%09 * 
 %0A%09 *
@@ -2335,16 +2335,128 @@
 nt type%0A
+%09 *%0A%09 * @see Proofs#emptyProof()%0A%09 * @see Inferences#isAsserted(Inference)%0A%09 * @see DynamicProof.ChangeListener%0A
 %09 */%0A%09pu
@@ -2513,16 +2513,20 @@
 etProof(
+%0A%09%09%09
 OWLAxiom
@@ -2537,20 +2537,17 @@
 ailment)
-%0A%09%09%09
+ 
 throws U

Improve javadoc