SPASS-Yarralumla

Published: 17 January 2019| Version 1 | DOI: 10.17632/r5t7gzv495.1
Contributors:
Renate Schmidt,

Description

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).

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.

Institutions

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

Categories

Software

Licence