IWIL 2012: Papers with AbstractsPapers 

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 plugins. Plugins 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 multiparadigm 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 hypertableaux, 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 firstorder 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 LEOII provers have pioneered the integration of higherorder and firstorder automated theorem proving. To date, the LEOII system is, to our knowledge, the only automated higherorder theorem prover which is capable of generating joint higherorder–firstorder proof objects in TPTP format. This paper discusses LEOII’s proof objects. The target audience are practitioners with an interest in using LEOII proofs within other systems. 

