Download current SPASS Prototypes and Experiments right now!

These pages provide very recent SPASS developments and experiments. More elaborate versions may eventually find their way into the SPASS distribution. In particular, be aware that the offered SPASS binaries my not be robust and documentation is not extensive. However, the SPASS prototype versions will at least perform the offered new functionality on the provided examples.

SPASS(LA) implementing superposition modulo linear arithmetic

PC Linux binary (SPASSLA.tgz, 0.6MB), including examples. The approach is based on the hierarchic theorem proving result by Bachmair, Ganzinger and Waldmann. Linear arithmetic constraint solving is performed via LP solving using QSopt. The package contains example problems formalizing properties of transition systems that can then be automatically proved by SPASS(LA). From the example files the extended SPASS syntax for linear arithmetic expressions can be easily derived. Please note that this SPASS(LA) version will crash when applied to non-linear problems and does not support equational reasoning. This will be fixed and added soon, respectively. SPASS(LA) will be contained in the next major release of SPASS.

Finite Domain Experiments

Here is a finite domain problem (LAN-FinDom.cnf) in SPASS dfg as well as in tptp syntax (LAN-FinDom.tptp). The problem formalizes part of the LAN infrastructure including Layer 3 IP addressing, router forwarding and stateful firewalling. It is satisfiable in a finite domain that in particular includes all 32 Bit IP addresses represented by 32 Bit bitvectors. Its a challenge problem for any prover targetting satisfiable finite domain problems, in particular if the prover is based on domain element instantiation.

SPASS with refined splitting

PC Linux binary (SPASSLS.tgz, 0.4MB). This version includes a refined splitting implementation, based on a refined backtracking procedure. On the average it performs 10% less splits compared to the current version SPASS 3.0. The refined splitting will be integrated into the next release of SPASS.

SPASS with contextual rewriting updated

PC Linux binary (SPASSCRW.tgz, 0.4MB). This version includes an implementation of approximated contextual rewriting together with an example clause set input file. It now includes a more sophisticated integration of the different rewriting rules plus fault caching. When activating contextual rewriting by the SPASS command line option "-RFRew=3" SPASS finitely saturates the example clause set. Without contextual rewriting (default setting) it diverges. By running SPASS with options "-RTaut=2 -RFRew=4 -RBRew=3" on the TPTP it solves 7 open problems (difficulty rating 1.0).