Re: SUO: a silly question about the new modular architecture
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