/*
 * #%L
 * Proof-Based Explanations
 * $Id:$
 * $HeadURL:$
 * %%
 * Copyright (C) 2011 - 2016 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%
 */
package org.liveontologies.protege.explanation.proof.service;

import org.liveontologies.puli.AssertedConclusionInference;
import org.liveontologies.puli.DynamicProof;
import org.liveontologies.puli.Inference;
import org.liveontologies.puli.ProofNode;
import org.liveontologies.puli.ProofStep;
import org.protege.editor.core.plugin.ProtegePluginInstance;
import org.protege.editor.owl.OWLEditorKit;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.reasoner.UnsupportedEntailmentTypeException;

/**
 * A skeleton for a plugin that can provide proofs for OWL axioms
 * 
 * @author Yevgeny Kazakov
 *
 */
public abstract class ProofService implements ProtegePluginInstance {

	private OWLEditorKit kit_;
	private String pluginId_;
	private String name_;

	public ProofService setup(OWLEditorKit kit, String pluginId, String name) {
		this.kit_ = kit;
		this.pluginId_ = pluginId;
		this.name_ = name;
		return this;
	}

	public OWLEditorKit getEditorKit() {
		return kit_;
	}

	public String getPluginId() {
		return pluginId_;
	}

	public String getName() {
		return name_;
	}

	@Override
	public String toString() {
		return getName();
	}

	/**
	 * @param entailment
	 * @return {@code true} if this service can provide a proof for the given
	 *         entailed {@link OWLAxiom}; the subsequent call of
	 *         {@link #getProof(OWLAxiom)} should return such a proof
	 */
	public abstract boolean hasProof(OWLAxiom entailment);

	/**
	 * Returns a proof for the given {@link OWLAxiom} as sets of inferences over
	 * {@link OWLAxiom}s. Using these inferences it should be possible to derive
	 * the given {@link OWLAxiom} from the axoioms in the ontology, if it is
	 * entailed. If the axiom cannot be derived, the result may be any inference
	 * set, e.g., the empty one.
	 * 
	 * @param entailment
	 *            the {@link OWLAxiom} for which the proof should be generated
	 * @return the {@link DynamicProof} representing the set of inferences using
	 *         which the given {@link OWLAxiom} can be derived from the axioms
	 *         in the ontology
	 * @throws UnsupportedEntailmentTypeException
	 *             if checking entailment of the given given {@link OWLAxiom} is
	 *             not supported
	 */
	public abstract DynamicProof<Inference<? extends OWLAxiom>> getProof(
			OWLAxiom entailment) throws UnsupportedEntailmentTypeException;

	/**
	 * This method provides examples that explain inferences used in the proof
	 * 
	 * @param inference
	 * 
	 * @return an example of the given inference, which can be used for
	 *         explanation purpose. Usually it is an inference instantiated with
	 *         some generic parameters. If {@code null}, no example is provided.
	 */
	abstract public Inference<? extends OWLAxiom> getExample(
			Inference<? extends OWLAxiom> inference);

	/**
	 * Using this method the displayed proof can be additionally post-processed
	 * before being displayed to the user
	 * 
	 * @param node
	 *            the {@link ProofNode} representing the acyclic proof tree
	 *            obtained from the proof returned by
	 *            {@link #getProof(OWLAxiom)}; the proof steps in this proof can
	 *            use only inferences from this proof or the
	 *            {@link AssertedConclusionInference} for inferences from the
	 *            axioms in the ontology. A {@link ProofNode} is acyclic if any
	 *            path induced by the conclusion -> premise relation in the
	 *            proof tree represented by this {@link ProofNode} does not
	 *            contain repetitions (i.e., equal {@link ProofNode}s).
	 * 
	 * @return the rewritten acyclic {@link ProofNode} that should be used to
	 *         display the proof
	 * 
	 * @see ProofStep#getInference()
	 */
	public ProofNode<OWLAxiom> postProcess(ProofNode<OWLAxiom> node) {
		return node;
	}

	@Override
	public abstract void dispose();

}

@@ -919,32 +919,113 @@
 puli.Inference;%0A
+import org.liveontologies.puli.Inferences;%0Aimport org.liveontologies.puli.Proof;%0A
 import org.liveo
@@ -1092,16 +1092,55 @@
 ofStep;%0A
+import org.liveontologies.puli.Proofs;%0A
 import o
@@ -2356,18 +2356,18 @@
 om%7D 
-as sets of
+containing
  inf
@@ -2404,32 +2404,20 @@
 om%7Ds
-. U
+ u
 sing 
-these inferences
+which
  it 
@@ -2444,20 +2444,16 @@
 o derive
-%0A%09 *
  the giv
@@ -2446,32 +2446,36 @@
 derive the given
+%0A%09 *
  %7B@link OWLAxiom
@@ -2479,32 +2479,63 @@
 iom%7D
- from the axo
+. In this proof, %7B@link OWLAx
 iom
+%7D
 s 
+occurring 
 in the
+%0A%09 *
  ont
@@ -2543,126 +2543,340 @@
 logy
-, if it is%0A%09 * entailed. If the axiom cannot be derived, the result may be any inference%0A%09 * set, e.g., the empty one.
+ can be derived using %7B@link AssertedConclusionInference%7D. If the%0A%09 * given %7B@link OWLAxiom%7D is not entailed, the result may be any proof in%0A%09 * which this %7B@link OWLAxiom%7D is not derivable, e.g., the empty proof.%0A%09 * %0A%09 * @see Proofs#isDerivable(Proof, Object)%0A%09 * @see Inferences#isAsserted(Inference)%0A%09 * @see Proofs#emptyProof()
 %0A%09 *
@@ -3053,16 +3053,16 @@
 s using%0A
+
 %09 *     
@@ -3116,52 +3116,8 @@
 ived
- from the axioms%0A%09 *         in the ontology
 %0A%09 *

Improve documentation