- From: Dan Connolly <connolly@w3.org>
- Date: Mon, 25 Jun 2001 10:30:17 -0500
- 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 UTC