Category: Inference engine
Example:
Last query in BaseKB :
(implies
(and
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL)))
(or
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL))))
Query reduced to True (a tautology).
Fine, but
Last query in BaseKB :
(implies
(and
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL)))
(or
(isa ?INST ?ACOL)
(isa ?INST ?BCOL)))
Query reduced to True (a tautology).
and
Last query in BaseKB :
(implies
(and
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL)))
(isa ?INST ?ACOL))
Query reduced to True (a tautology).
I.e. the inference engine is not sound.
However:
Last query in BaseKB :
(implies
(and
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL))
(isa ?ACOL Collection)
(isa ?BCOL Collection))
(isa ?INST ?ACOL))
Query halted because : Search space was exhausted.
Query was not proven
Last query in BaseKB :
(implies
(isa ?X ?COL)
(isa ?COL Collection))
Query halted because : Search space was exhausted.
Query was proven True [Explain]
Last query in BaseKB :
(implies
(and
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL))
(isa ?ACOL Collection)
(isa ?BCOL Collection))
(or
(not
(isa ?INST ?ACOL))
(not
(isa ?INST ?BCOL))))
Query halted because : Search space was exhausted.
Query was proven True [Explain]
Logged In: YES
user_id=564384
The above example suggests to us that with enough
redundant premises we can get rid of true or false tautology
answers, but the following are counterexamples:
Last query in BaseKB :
(implies
(and
(termOfUnit ?NOTCOL
(CollectionDifferenceFn Thing ?COL))
(isa ?X ?COL))
(not
(isa ?X ?NOTCOL)))
Query reduced to True (a tautology).
Last query in BaseKB :
(implies
(and
(termOfUnit ?NOTCOL
(CollectionDifferenceFn Thing ?COL))
(isa ?X ?COL)
(isa ?COL Collection)
(isa ?X Thing)
(isa ?NOTCOL Collection))
(isa ?X ?NOTCOL))
Query reduced to True (a tautology).
Logged In: YES
user_id=1085367
Sometimes a conditional query is deemed a tautology because
its antecedent is not WFF in the query Mt, and therefore (as
I understand it) the antecedent is treated as contradictory,
and hence the query is considered tautological. (I'm not
saying that makes sense, but I think that's how it currently
works...) You may want to check for that.
On the other hand, I and others have encountered many cases
where the antecedent is well-formed and the query is still
deemed a tautology. I am not sure of the cause. This is a
known (and, to me, particularly annoying) bug that will (I
hope) be fixed in the near future.