This folder contains the interface to the SoftFOL provers. Currently there are three prover interfaces available: SPASS, the MathServ Broker and Vampire whereas the latter is called via MathServ, too. The MathServ Broker chooses the best prover depending on the problem, as there are E, Otter, SPASS, Vampire.

The folder will be renamed to SoftFOL when the repository's version administrating system changes from CVS to Subversion.

The SPASS project homepage is located at http://spass.mpi-sb.mpg.de/.

SoftFOL.Sign provides data structures for SoftFOL signatures, formulae and problems.

The emphasis is on outputting theories with the pretty printer (SoftFOL.Print); hence, not only the kernel language of SPASS is supported. Because the SPASS logic is only used for proving, no parser and static analysis are provided.

SoftFOL.ProveSPASS is an interactive (SPASS is fully automated) interface to the SPASS prover. It uses genericATPgui for display and interaction.

SoftFOL.ProveMathServ is similar to SoftFOL.ProveSPASS as it addresses the MathServ Broker using the same GUI. The prover result (given by MathServ response) will be parsed and mapped into GenericConfig prover structures.

SoftFOL.ProveVampire is quite similar to SoftFOL.ProveMathServ, using MathServ for adressing the Vampire prover.

SoftFOL.MathServParsing provides functions for parsing a MathServ output into a MathServResponse structure.

SoftFOL.MathServMapping maps a MathServResponse into a GenericConfig structure.

SoftFOL.ProverState provides data structures and initialising functions for Prover state and configurations.

SoftFOL.Logic_SoftFOL provides the SoftFOL instance of type class Logic.

SoftFOL.ATC_SoftFOL: Automatic ATC derivation

SoftFOL.Conversions provides functions to convert to internal SP* data structures.

SoftFOL.CreateDFGDoc prints a (G_theory CASL _) into a DFG Doc.

SoftFOL.Translate provides collection of functions used by Comorphisms.SuleCFOL2SoftFOL and all prover interfaces (SoftFOL.ProveSPASS, SoftFOL.ProveMathServ, SoftFOL.ProveVampire, SoftFOL.ProveDarwin) for the translation of CASL identifiers and axiom labels into valid SoftFOL identifiers.

SoftFOL.Print arranges pretty printing for SoftFOL signatures in DFG syntax. Refer to http://spass.mpi-sb.mpg.de/webspass/help/syntax/dfgsyntax.html for the DFG syntax documentation.

SoftFOL.PrintTPTP arranges pretty printing for SoftFOL signatures in TPTP syntax. Refer to http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html for the TPTP syntax documentation.

Relevant papers on SPASS include:

C. Weidenbach, Spass: Combining superposition, sorts and splitting, in Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, 1999.