spass
automated theorem prover for first-order logic with equality
Command lineScience
Not tested on a device yet. What that means
Commands in the package
SPASSFLOTTER
About spass
From Debian's package 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.
From Debian's description of the spass package, under that package's license.
Dependencies
Depends on
libc6
Related apps
- coqproof assistant for higher-order logic (toplevel and compiler)Command line
- z3theorem prover from Microsoft ResearchCommand line
- hol-lightHOL Light theorem proverCommand line
- cvc4automated theorem prover for SMT problemsCommand line
- eproverEquational theorem proverCommand line
- monatheorem prover based on automataCommand line
Sources and licenses
- Name: the Debian package name.
- Summary: Debian's short description of the spass package, under that package's license.
- Description: Debian's description of the spass package, under that package's license.
- Versions and sizes: Debian's archive for ARM64, as on packages.debian.org.
- Popularity: Debian Popularity Contest counts.
More in About the catalog.