spass

automated theorem prover for first-order logic with equality

Description

SPASS is a saturation-based automated theorem prover for first-order logic with equality. It is unique due to the combination of the superposition calculus with specific inference/reduction rules for sorts (types) and a splitting rule for case analysis motivated by the beta-rule of analytic tableaux and the case analysis employed in the Davis-Putnam procedure. Furthermore, SPASS provides a sophisticated clause normal form translation.

This package consists of the SPASS/FLOTTER binary, documentation, and a small example collection. The tools collections contain the proof checker pcs, the syntax translators dfg2otter and dfg2tptp, and the ASCII pretty printer dfg2ascii.

Upload more screenshots

Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.

Upload a screenshot

Hint: upload an image here from your clipboard with Ctrl-V


Homepage

http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover/


Install this software package

If the package is available for the distribution you are currently using on your computer then install the software by clicking on…

Install spass