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

Re: Inconsistency in KIF's list specification

From: Dan Connolly <connolly@w3.org>
Date: Mon, 25 Jun 2001 10:30:17 -0500
Message-ID: <3B375909.7280441F@w3.org>
To: Ken Baclawski <kenb@ccs.neu.edu>
CC: www-rdf-logic@w3.org
Ken Baclawski wrote:
> 
> 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>.

Fascinating. One minute I'm catching up on the morning's
email, and suddenly I realize I've spent an (unscheduled!)
hour poring over that stuff. Oops!

One thing I kept looking for, without finding it,
was source code. Can I get my hands on SNARK etc.?
  http://www.ai.sri.com/~stickel/snark.html

Are any of these tools Open Source?

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Monday, 25 June 2001 11:30:19 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:40 GMT