Add positive test cases to ontology which are not entailed anymore after a repair

From "OntoDebug: Interactive Ontology Debugging Plug-In for Protégé" on page 5 we state that

However, the application of diagnosis D₁ results in a new ontology O₁ := O ∖ D₁ that, along with B, does not entail B(v) as required by the set of positive test cases. Consequently, O₁ must be extended with some set of axioms EX such that O1 ∪ EX fulfills all requirements to O*. Of course, the intended set EX is unknown to the debugger and possibly some complex learning methods must be used to obtain it. One solution [20, Prop. 3.5] to this problem is to approximate EX with the set of positive test cases P, which comprises all necessary entailments of O*. In our example the ontology O₁ ∪ P satisfies all test cases. Hence, in order to specify O* the user must extend the ontology O₁ with the assertion B(v) or axioms entailing B(v).

This feature has to be implemented.

When a diagnosis is found the diagnosis considers the positive test cases,but after the repair of the diagnosis, the entailment of a positive test case might disappear.

This has to be checked for each positive test case after the repair and the user has to be asked if she wants to add those axiom explicitely to the ontology.