Published: 17 Jan 2019 | Version 1 | DOI: 10.17632/r5t7gzv495.1

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.

Latest version

  • Version 1


    Published: 2019-01-17

    DOI: 10.17632/r5t7gzv495.1

    Cite this dataset

    Schmidt, Renate; Baumgartner, Peter (2019), “SPASS-Yarralumla”, Mendeley Data, v1


Views: 29
Downloads: 6


The University of Manchester, Australian National University, Data61, Max-Planck-Institut fur Informatik




CC BY 4.0 Learn more

The files associated with this dataset are licensed under a Creative Commons Attribution 4.0 International licence.

What does this mean?
You can share, copy and modify this dataset so long as you give appropriate credit, provide a link to the CC BY license, and indicate if changes were made, but you may not do so in a way that suggests the rights holder has endorsed you or your use of the dataset. Note that further permission may be required for any content within the dataset that is identified as belonging to a third party.