Home
Linux temps réel embarqué et outils de développements Technique





spass

spass An automated theorem prover for first-order logic with equality
Priority
Sectionscience
Installed size 2188
Maintainer Roland Stigge <stigge@antcom.de>
Architecture i386
Version 2.1-3
Depends libc6 (>= 2.3.2-1)
Suggests spamassassin
File name pool/main/s/spass/spass_2.1-3_i386.deb
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. . For more information, additional and partly huge example collections, consider the project homepage at http://spass.mpi-sb.mpg.de/.


©M.N.I.S Société | Produits | Services | Formations | Support | Partenariat | Presse | Téléchargements ©M.N.I.S