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

RE: Inconsistency in KIF's list specification

From: Kogut, Paul A <paul.a.kogut@lmco.com>
Date: Thu, 28 Jun 2001 09:32:33 -0400
To: "'Dan Connolly'" <connolly@w3.org>, Ken Baclawski <kenb@ccs.neu.edu>
Cc: www-rdf-logic@w3.org
Message-id: <079B626B05A0D3118B1000508B0EA5E904CD4FAF@emss04m05.ems.lmco.com>
Richard used Specware as a front end to SNARK (see his explanation below).
SNARK is distributed with Specware along with another theorem prover called
Gandalf.
Specware can be obtained from the Kestrel Institute for research purposes
for a small fee.

Paul Kogut
Lockheed Martin
UBOT Project 

SNARK is not a finished system and no policy has been established for its
distribution. The system is not fully documented and does not have a
graphical interface. In the past,  Mark has given it--as is--to people using
it for research purposes, on a case-by-case basis, and he would like to see
it become open source.

I made good use of the Specware Interface.  Raw Snark has no structure
corresponding to a theory, in which a sequence of axioms and conjectures is
presented, each proof depending on the previous sentences in the sequence.
Also I think Specware's facilities for combining theories and for mapping
one theory into another is important for DAML.

There would be some reason to use SNARK as is.  One would get access to some
features that are currently inaccessible through the interface.  Also SNARK
can read formulas in KIF, but Specware cannot.


> -----Original Message-----
> From:	Dan Connolly [SMTP:connolly@w3.org]
> Sent:	Monday, June 25, 2001 11:30 AM
> To:	Ken Baclawski
> Cc:	www-rdf-logic@w3.org
> Subject:	Re: Inconsistency in KIF's list specification
> 
> 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 Thursday, 28 June 2001 09:31:33 GMT

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