I start with a virgin image.

Create ColSub, ColSuper, and assert both to be

instances of Collection.

All in BaseKB.

A step aside:

Assert: (isa ColSuper FirstOrderCollection)

Assert (Monotonic-Backward): (genls ColSub ColSuper).

Ask: (isa ColSub FirstOrderCollection)

Cannot make the system prove it.

!Retract: (genls ColSub ColSuper)

End of the step aside.

!Assert (Monotonic-Backward):

(implies (isa ?X ColSub) (isa ?X ColSuper))

Ask: (genls ColSub ColSuper)

Cannot make the system prove it, even if the rule

(implies (isa ?X ColSub) (isa ?X ColSuper)) is given to

the proof checker and allowed.

Ask trivially:

Mt : BaseKB

EL Query :

(implies

(isa ?X ColSub)

(isa ?X ColSuper))

Justifications :

(implies

(isa ?X ColSub)

(isa ?X ColSuper)) in BaseKB

:ISA (isa HYP-ColSub-8884 ColSub) in Proof-

HypotheticalContext-8888

Note:

1. (isa HYP-ColSub-8884 ColSub) is not needed in this

proof.

2. The parameters were: 1 transformation step, HL

predicate transformation allowed.

3. If this is reset to No Transformation and HL predicate

transformation not allowed,

then Suspended, Exhaust, No Answer

4. In an image with a longer history I could not at all

make the system prove

this directly asserted rule. Therefore I started for this

example with a virgin image.

Ask:

(trueSentence

(implies

(isa ?X ColSub)

(isa ?X ColSuper)))

Cannot find a parameter setting such that the system

finds a proof of this!

It has several times been complained by me

that expansion axioms are not more effective than

comments.

Therfore I add the following rule for genls (Monotonic

Backward)

(implies

(implies (isa ?Obj ?Col1) (isa ?Obj ?Col2))

(genls ?Col1 ?Col2))

This is transformed by the system into the nonsense

a)

(implies

(isa ?OBJ ?COL2)

(genls ?COL1 ?COL2))

b)

(or

(isa ?OBJ ?COL1)

(genls ?COL1 ?COL2))

a) or b) can each be retracted without the system

retracting the other.

Confer the typical thread in the Open Discussion Forum

starting from my mail "A rule transformation bug" on

2002-06-18 13:04.

This implicit, but not acknowledged bug report pertained

to Release 0.6 !

I retract a) and b) and assert:

(implies

(trueSentence

(implies

(isa ?Obj ?Col1)

(isa ?Obj ?Col2)))

(genls ?Col1 ?Col2))

This works to avoid the nonsense canonicalization.

Now I ask:

(genls ColSub ColSuper)

and cannot find a parameter setting such that I get a

positive answer,

even if present the pertinent rule to the proof checker

on the tablet.

The Query Tool answers always with No answer and

suspended, Exhaust.

Legacy Ask shows the pertinent rule always (!) as its

last child of the inference tree,

and when its antecedent is used in a "Socratic Ask" I

end up as above with the Query tool.

Is anybody there who reads this and willing to throw

some light on it?