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:


Download spass_yarr.tgz and unpack with

tar -zxvf spass_yarr.tgz
and refer to the README file. Runs on Linux platforms.


We look forward to your feedback. Please send your comments and suggestions to
Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 23 Nov 16
Copyright © 2008-2016 Renate A. Schmidt, School of Computer Science, Man Univ,