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?
Dietrich H. Fischer
2004-03-12
Logged In: YES
user_id=564384
PS
In Note 2 above I should have said:
The system did not answer True with the default parameter
setting, and answered True only, when I set the parameters
as said above in Note 2.
Then the system has entered into the following proof
(my Note 1 was blind to that):
It takes a hypothetical x and assumes the antedecent with
that. Then knowing the rule it can conclude its consequent,
and thus prove the implication.
The system is not prepared for my "stupid" question which
just wants just to return thruth for what has been asserted.
That might be pardonable, but not only for (trueSentence ...)
No answer - Suspended, Exhaust
is returned, but also for:
Status : Suspended, Exhaust Total
Mt : BaseKB
EL Query :
(assertedSentence
(implies
(isa ?X ColSub)
(isa ?X ColSuper)))
No answers
Dietrich H. Fischer
2004-03-26
Logged In: YES
user_id=564384
With respect to
Ask:
(trueSentence
(implies
(isa ?X ColSub)
(isa ?X ColSuper)))
given that
(implies (isa ?X ColSub) (isa ?X ColSuper)) was asserted
I found out the following:
The systems tries to find some ?X wich makes the implication
true!
And that is fulfilled if some constant XX is instance in both
collections,
for example, just by asserting that,
or by declaring (implies (isa ?X ColSub) (isa ?X ColSuper)) as
Forward
and asserting (isa XX ColSub),
but not by asserting (isa XX ColSub)
and having (implies (isa ?X ColSub) (isa ?X ColSuper)) only as
Backward!
Mt : BaseKB
EL Query :
(trueSentence
(implies
(isa ?X ColSub)
(isa ?X ColSuper)))
Show Hide Answers (1 new)
Answer ?X
*[Explain] Lea
Therefore I retracted the rule
(implies
(trueSentence
(implies
(isa ?Obj ?Col1)
(isa ?Obj ?Col2)))
(genls ?Col1 ?Col2))
and asserted instead
(implies
(trueSentence
(forAll ?Z
(or
(isa ?Z ?Y)
(not
(isa ?Z ?X)))))
(genls ?X ?Y))
However, that did not help to infer
(genls ColSub ColSuper) or even to prove
(#$trueSentence
(#$forAll ?X
(#$implies
(#$isa ?X #$ColSub)
(#$isa ?X #$ColSuper)))),
giventhat
(#$forAll ?X
(#$implies
(#$isa ?X #$ColSub)
(#$isa ?X #$ColSuper)))
was directly asserted.
PS.
The canonicalization of
(implies
(implies (isa ?Obj ?Col1) (isa ?Obj ?Col2))
(genls ?Col1 ?Col2))
in fact is ok,
i.e., as I was told,
my expression for the intended implication is not ok.
That may be a good example for learners.