[Pellet-users] explanation

[Hongkai Liu]

Hello,

I have been using Pellet to give an explanation of inconsistent ABox.
I found out the ABox assertion given by Pellet does not syntactically
equal to the one in the input ABox. Here is the input:

(DEFINE-PRIMITIVE-ROLE R_SPOUSE)
(DEFINE-PRIMITIVE-ROLE R_HASP)
(INSTANCE IND_JOHN (OR (NOT (AND (OR HAPPY (OR (ONE-OF IND_MARY)
(ONE-OF IND_JOHN))) (NOT (NOT TOP)))) (AND (OR (OR (ONE-OF IND_MARY)
(ONE-OF IND_JOHN)) (ALL R_SPOUSE (OR (NOT (AND (OR HAPPY (OR (ONE-OF
IND_MARY) (ONE-OF IND_JOHN))) (NOT (NOT TOP)))) (NOT (ONE-OF
IND_MARY))))) (ALL R_SPOUSE (OR (OR (ONE-OF IND_MARY) (ONE-OF
IND_JOHN)) (OR (NOT (AND (OR HAPPY (OR (ONE-OF IND_MARY) (ONE-OF
IND_JOHN))) (NOT (NOT TOP)))) (NOT (ONE-OF IND_MARY))))) (AND (OR (NOT
(ONE-OF IND_JOHN)) (ALL R_SPOUSE (OR (NOT (ONE-OF IND_JOHN)) (OR (NOT
(AND (OR HAPPY (OR (ONE-OF IND_MARY) (ONE-OF IND_JOHN))) (NOT (NOT
TOP)))) (NOT (ONE-OF IND_MARY)))))) (OR (NOT (ONE-OF IND_JOHN)) (ALL
R_SPOUSE (OR (NOT (ONE-OF IND_MARY)) (OR (NOT (AND (OR HAPPY (OR
(ONE-OF IND_MARY) (ONE-OF IND_JOHN))) (NOT (NOT TOP)))) (NOT (ONE-OF
IND_MARY)))))) (OR (NOT (ONE-OF IND_MARY)) (ALL R_SPOUSE (OR (NOT
(ONE-OF IND_JOHN)) (OR (NOT (AND (OR HAPPY (OR (ONE-OF IND_MARY)
(ONE-OF IND_JOHN))) (NOT (NOT TOP)))) (NOT (ONE-OF IND_MARY)))))) (OR
(NOT (ONE-OF IND_MARY)) (ALL R_SPOUSE (OR (NOT (ONE-OF IND_MARY)) (OR
(NOT (AND (OR HAPPY (OR (ONE-OF IND_MARY) (ONE-OF IND_JOHN))) (NOT
(NOT TOP)))) (NOT (ONE-OF IND_MARY))))))) TOP)))
(RELATED IND_JOHN IND_MARY R_SPOUSE)

-------------------------
I call Pellet with the following method:

public void consistent (String Name, boolean UNA) {
		if (UNA)
			PelletOptions.USE_UNIQUE_NAME_ASSUMPTION = true;
		else
			PelletOptions.USE_UNIQUE_NAME_ASSUMPTION = false;
		PelletOptions.USE_TRACING = true;
        KnowledgeBase kb = new KnowledgeBase();
        kb.setDoExplanation( true );
        KRSSLoader loader = new KRSSLoader();
        try{
        loader.load( Name , kb );
        }catch (Exception e){
			System.err.println("Error: " + e.getMessage());
		}
        kb.prepare();
        //System.out.println( "Expressivity: " + kb.getExpressivity() );

        boolean consistent = kb.isConsistent();

        System.out.println( "Consistent  : " + (consistent?"Yes":"No") );

        if(!consistent) {
        	Set<aterm.ATermAppl> exp = kb.getExplanationSet();
        	myPrinter.printATermAxioms(exp);
        }
        //*/
		
	}

--------------------
Here is the output of

 WARN [main] (KnowledgeBase.java:1573) - Inconsistent ontology.
Reason: Individual IND_JOHN is forced to belong to class
and([not(value(IND_JOHN)),not(HAPPY),not(value(IND_MARY))]) and its
complement
 WARN [main] (KnowledgeBase.java:1575) - ExplanationSet:
[type(IND_JOHN,or([and([_TOP_,and([or([all(R_SPOUSE,or([or([not(value(IND_MARY)),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))]),not(value(IND_MARY))])),not(value(IND_MARY))]),or([all(R_SPOUSE,or([or([not(value(IND_MARY)),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))]),not(value(IND_JOHN))])),not(value(IND_MARY))]),or([all(R_SPOUSE,or([or([not(value(IND_MARY)),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))]),not(value(IND_MARY))])),not(value(IND_JOHN))]),or([all(R_SPOUSE,or([or([not(value(IND_MARY)),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))]),not(value(IND_JOHN))])),not(value(IND_JOHN))])]),all(R_SPOUSE,or([or([not(value(IND_MARY)),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))]),or([value(IND_JOHN),value(IND_MARY)])])),or([all(R_SPOUSE,or([not(value(IND_MARY)),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))])),or([value(IND_JOHN),value(IND_MARY)])])]),not(and([not(not(_TOP_)),or([or([value(IND_JOHN),value(IND_MARY)]),HAPPY])]))])),
prop(R_SPOUSE,IND_JOHN,IND_MARY)]

The first assertion pinpointed by Pellet (1.5.1) is not any one in the
input ABox. I did not check weather it is equivalent semantically to
some one in the input. I knew that Pellet does pinpointing with "not
top" instead of "bottom". I would like to let Pellet give me the
explanantion which is a subset of the original ABox. Changing bottom
to not top is ok since I can modify the input. However, it seems that
Pellet also changes other things. Is that true? Is there any global
variable setting this up?

Best regards.

Hongkai Liu