W3C home > Mailing lists > Public > www-rdf-logic@w3.org > June 2001

Inconsistency in KIF's list specification

From: Ken Baclawski <kenb@ccs.neu.edu>
Date: Mon, 25 Jun 2001 10:14:22 -0400 (EDT)
To: www-rdf-logic@w3.org
Message-ID: <Pine.LNX.3.96.1010625101222.7354I-100000@steam>
The UBOT project has found an inconsistency in the axioms for lists
in the Knowledge Interchange Format (KIF). The inconsistency was
discovered by Richard Waldinger, who used the Specware tool with the
SNARK automatic theorem prover.  More specifically, the axiom that
defines the 'first' function has a quantifier error, and
unintentionally implies that all elements are equal.

For more information about this inconsistency as well as
inconsistencies in DAML+OIL see: <http://vis.home.mindspring.com>.

The inconsistency was discovered while checking the consistency of
DAML+OIL whose axiomatic semantics is expressed using KIF.  It was a
surprise when an apparent inconsistency in DAML+OIL turned out to be
the result of an inconsistency in KIF itself.  It was even more
surprising to discover that the inconsistency is not in an obscure
part of KIF, such as list iterators, but in the fundamental list
function that extracts the first element of a list.

What is striking about this inconsistency is that KIF has been in use
for years (even to the point of being a draft American National
Standard), yet this inconsistency has not yet surfaced.  It indicates
how hard it is for a person to anticipate what logical formulas imply
just by looking at them.

Ken Baclawski
UBOT Project
Received on Monday, 25 June 2001 10:14:37 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:35 UTC