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 : Tuesday, 27 October 2009 08:34:46 GMT