#20 “Tautology” answers considered harmful

open
nobody
None
5
2003-01-28
2003-01-28
No

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]

Discussion

  • 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
    Casey McGinnis
    2005-02-10

    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.