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
and refer to the README file.
Runs on Linux platforms.
Feedback
We look forward to your feedback. Please send your comments and suggestions
to
schmidt@cs.man.ac.uk.
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, schmidt@cs.man.ac.uk