Re: SUO: a silly question about the new modular architecture
John,
Yes, there are lots of theorem provers and PTTP is a good one too. I've
talked with Mark about it. I was referring to Seth's request below for
quite a different set of tools. He wasn't simply requesting a theorem prover.
> > I believe that the most
> > useful SUMO would have a front end tool where the ~user~ answers a set of
> > questions and clicks on a set of contexts .. the tool would then generate
> > the needed ontology. Then where certain axioms were still
> unacceptable, one
> > could replace them individually ... the tool would then thread through the
> > selected knowledge and delete any contradictions and suggest where new
> > axioms were needed.
>
>There are already very good off-the-shelf tools for doing those kinds
>of things.
Adam
At 09:13 PM 8/31/2001 -0400, John F. Sowa wrote:
>Adam,
>
>The most widely used theorem prover is Otter, which has been
>available as free download in source form (C code) for years.
>It also accepts input in KIF. Following is the URL:
>
> http://www-unix.mcs.anl.gov/AR/otter/
>
>But you might also ask Mark Stickel. He's more of an expert in the
>field that I am. He has his own theorem prover (which he'll give
>you if you aks him). His isn't as fast as Otter, but it also takes
>input in KIF, and Mark can give you more info about the pluses and
>minuses of essentially all the tools in the area.
>
>John
Adam Pease
Teknowledge
(650) 424-0500 x571