- From: Ken Baclawski <kenb@ccs.neu.edu>
- Date: Mon, 25 Jun 2001 10:14:22 -0400 (EDT)
- To: www-rdf-logic@w3.org
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 Ken@Baclawski.com
Received on Monday, 25 June 2001 10:14:37 UTC