SPASS Workbench

Starting from Version 4.0 SPASS is no longer distributed as a monolithic first-order theorem prover but as a workbench of tools where the successor of the classic prover is simply one component. The development of the SPASS workbench is bottom up, we distribute binaries of our tools in the order they get ready, starting with tools for "simple" logics.

The currently available tools of the workbench are:

• the old classic SPASS theorem prover: SPASS 3.9 providing a WebInterface
• the SPASS LIA theory solver: SPASS-IQ
• the SPASS ground arithmetic solver: SPASS-SATT
• the SPASS SAT CDCL solver SPASS-SAT with explicit reduction providing a Webinterface
• the SPASS-CNF propositional CNF converter providing a Webinterface