Automation of Logic
English

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.

Generalized Renaming

  • Here are the translations of 526 TPTP 5.4.0 formula problem files (genrenaming.tgz, 2400KB) where generalized renaming achieves a reduction of at least 5% in the number of clauses compared to standard renaming.

SPASS(iSAT) on collision avoidance protocols

  • TGZ archive (colprot.tgz, 550KB), including all collision avoidance protocol experiments: input files as well as SPASS(iSAT) output files.

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-Y2

SPASS-YAGO++

  • SPASS-YAGO++ 64-Bit Linux binaries plus all example files including the YAGO++ ontology ( Yago++.cnf.gz, 248MB) and its finite saturation ( Yago++.cnf.model.gz, 252MB), as well as the queries ( Yago++-queries.tgz, 693B). The SPASS-YAGO++ binary (SPASS-YAGO++.gz, 359KB). The dfg2tptp binary can be loaded from the SPASS-YAGO distribution above. For saturation call "SPASS-YAGO++ Yago++.cnf" and for a query the two successive commands "SPASS-YAGO++ Yago++.cnf.model -Server &" and "cat query.dfg > SYFIFOIN".

DHCP Reachability Probability Analysis via FPTA

  • First-order probabilistic timed automata (FPTA) are a generalization of probabilistic timed automata (PTA) with first-order theories. The archive (dhcp.tgz 4kB) contains the FOL(LA) theory of an FPTA describing DHCP, the MoDeST code of the generated VPTA out of the reachability proofs for the DHCP bound state, analyzed by mcpta, and the resulting PRISM model for the eventual reachability probability analysis.