#20 “Tautology” answers considered harmful

[Dietrich H. Fischer]

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]

[Dietrich H. Fischer]

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).

[Casey McGinnis]

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.