SPASS

From Wikipedia, the free encyclopedia
Jump to: navigation, search

SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. It is released under the FreeBSD license.[1]

[edit] References

  • Weidenbach, Christoph; Schmidt, Renate; Hillenbrand, Thomas; Rusev, Rostislav; Topic, Dalibor (2007), "System Description: SPASS Version 3.0", Automated Deduction -- CADE-21 : 21st International Conference on Automated Deduction, Springer, pp. 514–520 .

[edit] External links

Personal tools
Namespaces
Variants
Actions
Navigation
Interaction
Toolbox
Print/export