IWIL 2012: Papers with Abstracts

Abstract. Modern Satisfiability Modulo Theories (SMT)
solvers are fundamental to many program
analysis, verification, design and testing tools. They are a good
fit for the domain of software and hardware engineering because
they support many domains that are commonly used by the tools.
The meaning of domains are captured by theories that can be
axiomatized or supported by efficient <i>theory solvers</i>.
Nevertheless, not all domains are handled by all solvers and
many domains and theories will never be native to any solver.
We here explore different theories that extend Microsoft
Research's SMT solver Z3's basic
support. Some can be directly encoded or axiomatized,
others make use of user theory plug-ins.
Plug-ins are a powerful way for tools to supply their custom domains.

Abstract. Craig interpolation is a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. Over the last years, a variety of interpolation procedures for linear integer arithmetic (and extensions) have been developed. I will give an overview of the existing algorithms and design choices, and then discuss implementations of such procedures within theorem provers and SMT solvers. In particular, I will describe an implementation done using the multi-paradigm language Scala, which is built on top of the Java runtime infrastructure, and evaluate performance and engineering aspects.

Abstract. Over the past decades, a number of calculi for automated
reasoning have been proposed that share some core features:
1. proofs are built in a tableau/sequent style as trees where
nodes are labeled with literals, and 2. these proofs are expanded
by interpreting the problem clause set as a set of rules, and
requiring all negative literals in clauses to present on a branch
for expansion. This applies to hyper-tableaux, MGTP, coherent
logic, and others. Existing implementations typically spend much
of their time in the process of matching branch literals with the
negative literals of the input clauses. We present an
alternative to this matching process by applying a modified
version of the RETE algorithm. The RETE algorithm was developed
in the 1970s for production systems in artificial
intelligence. We exploit the similarities between the mentioned
calculi and production systems in order to make the RETE
algorithm solve the matching problem. We also investigate the
effect of working on several independent branches present in
tableau proof search but not in production systems.

Abstract. An implementation of an automated theorem prover for first-order modal logic is presented that works for the constant, cumulative and varying domains of the modal logics D, T, S4 and S5. It is based on the (classical) connection calculus and uses prefixes (or world paths) and a prefix unification algorithm to capture the restrictions given by the Kripke semantics of the standard modal logics. This permits a modular and elegant treatment of the considered modal logics and yields an efficient implementation. Details of the calculus, the implementation and performance results on the QMLTP problem library are presented.

Abstract. The LEO and LEO-II provers have pioneered the integration of higher-order and first-order automated theorem proving. To date, the LEO-II system is, to our knowledge, the only automated higher-order theorem prover which is capable of generating joint higher-order–first-order proof objects in TPTP format. This paper discusses LEO-II’s proof objects. The target audience are practitioners with an interest in using LEO-II proofs within other systems.