This site offers initial functionality in order to run proofs of first-order theorems using the theorem prover OTTER.
OTTER is an automated deduction system designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs.
This site is intended as a test platform for GnosioGenesis. At the moment, it simply provides a web interface to GnosioGenesis' inference engine, OTTER.
At this stage, input files can be uploaded to the server and submitted to the theorem prover. Results are then displayed in a web page. Because we will be using OTTER directly at this stage, the conclusion and the assumptions for a given proof will have to reside on the same file. In general, researchers are interested in checking whether a number of conclusions follows from the same set of assumptions. This will be possible when the database for the system is operational.
The next step in the GnosioGenesis project is the integration of the database with OTTER. First-order logic statements in this databases will be linked to corresponding statements in English. These statements can be combined at will in order to automatically generate the input files for OTTER. Proofs generated by OTTER can then be translated back to English statements in a similar fashion.
For full information about OTTER, please visit OTTER's web site.