OpenCyc

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?