Description of this data
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. To appear in the Journal of Automated Reasoning. The short version appears 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).
Experiment data files
Steps to reproduce
Download spass_yarr.tgz, unpack with
tar -zxvf spass_yarr.tgz
and refer to the README file. Runs on Linux platforms.
Cite this dataset
Schmidt, Renate; Baumgartner, Peter (2019), “SPASS-Yarralumla”, Mendeley Data, v1 http://dx.doi.org/10.17632/r5t7gzv495.1
The files associated with this dataset are licensed under a Creative Commons Attribution 4.0 International licence.