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.
Authorization Analysis
- The dfg file(sap.dfg, 0.45KB) includes a first-order
theory representing the formalization of an SAP R/3 authorization and process setup together with business
policies for a purchase process.
(SAP and SAP R/3 are registered trademarks of SAP AG in Germany and other countries.)
Disunification and Predicate Completion with SPASS
SPASS-YAGO
- SPASS-YAGO and dfg2tptp 64-Bit Linux binaries plus all slice example files (spassyagoslice.tgz, 216MB).
The overall YAGO core together with the two query examples is here (fullqueries.tgz, 767MB).
