SPASS-Yarralumla

SPASS-yarralumla is a first-order theorem prover. It implements sophisticated forms of blocking and other enhanced techniques for bottom-up model generation. The implementation is based on an adaptation of the SPASS prover and formula transformations implemented in Yarralumla.

Details of the theory, proofs, the implementation and results of an empirical evaluation on problems from the TPTP benchmark suite can be found here:

• Blocking and Other Enhancements for Bottom-Up Model Generation Methods. P. Baumgartner and R. A. Schmidt. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139 (2006).
  Abstract, Full text via Springer, BiBTeX.
• The extended long version is under review for publication.

Download

Download spass_yarr.tgz and unpack with

tar -zxvf spass_yarr.tgz

Feedback