PAAR on Wednesday, July 14th

09:00‑10:00 Invited talk by Larry Paulson and Jasmine Christian Blanchette
Location: AT 2.14
09:00 Jasmine Christian Blanchette (TU München)
Invited talk: Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers

Sledgehammer is a highly successful tool that makes automatic theorem provers available to an interactive theorem prover (Isabelle). It requires no user configuration: it can be invoked with a single mouse gesture at any point in the proof. It automatically finds any lemmas it requires from those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle proof script: its output cannot be trusted, but it does not need to be trusted. Sledgehammer turns out to work particularly well with structured proofs, making it easy for beginners to construct substantial proofs. The invited talk will review the development of Sledgehammer and describe its impact on the Isabelle community.

10:30‑12:30 Session 1
Location: AT 2.14
10:30 Laura Meikle and Jacques Fleuriot
Automation for Geometry in Interactive Theorem Provers

In this paper we describe a number of automation techniques which we have developed to assist us in reasoning formally about geometry in the interactive theorem prover Isabelle. These range from simplification rules to a user-centric integration of Isabelle with the computer algebra system QEPCAD-B. We demonstrate the power and limitations of these techniques through illustrative examples taken from our verification of a triangulation algorithm.

11:00 Andrew Matusiwicz, Neil Murray and Erik Rosenthal
Trie Based Subsumption and Improving the pi-Trie Algorithm

An algorithm that stores the prime implicates of a logical formula in a trie was developed in \cite{mmr09}. In this paper, an improved version of that $pi$-trie algorithm is presented. It achieves its speedup primarily by significantly decreasing subsumption testing. Preliminary experiments indicate the new algorithm to be substantially faster and the trie based subsumption tests to be considerably more efficient than the clause by clause approach originally employed.

11:30 Guido Fiorino
Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus

We present a procedure to decide propositional Dummett logic. Such a procedure relies on a tableau calculus with a multiple premise rule and optimizations. The resulting implementation outperforms the state of the art graph-based procedure.

12:00 Thomas Bouton, Diego Caminha, David Deharbe and Pascal Fontaine
GridTPT: a distributed platform for Theorem Prover Testing

Programming provers is a complex task; completeness or even soundness may often be broken by apparently harmless bugs. A good testing platform can contribute in detecting problems early and helping development. This paper presents the distributed platform for testing the veriT SMT solver. Its features are fairly standard, but it allows to easily distribute the task in a cluster.

We plan to distribute this platform as an open source tool for the community of developers of automated theorem provers. This presentation to PAAR'2010 would provide the opportunity to discuss the need for such a tool and the necessary features in a broader context. We would like to extract a requirement specification from this discussion, that would be useful to get dedicated implementation resources for distribution, maintenance and future development of the tool.

14:00‑15:00 Invited talk by Andrei Voronkov
Location: AT 2.14
14:00 Andrei Voronkov (University of Manchester)
Invited Talk: Vampire: the Fresh Blood

The first version of the theorem prover Vampire was implemented 17 years ago. Vampire has always been known for its fast implementation, for example it has won 20 world cup winner titles in first-order theorem proving. In this talk we will overview the results of a complete re-design of Vampire made in the last 1.5 years. Vampire has become even faster and includes several new features that makes it an ideal tool for applications: reasoning with theories, generation of colored proofs, interpolant generation, and reasoning with very large theories.

The talk is based on joint work with Krystof Hoder and Laura Kovacs.

15:30‑17:35 Session 2
Location: AT 2.14
15:30 Djihed Afifi, David Rydeheard and Howard Barringer
Automated Reasoning in the Simulation of Evolvable Systems

We present a novel application of automated theorem proving for the simulation of computational systems. The computational systems we consider are evolvable, i.e. may reconfigure their structure and programs at run-time. In [1], a logical framework for describing such systems is introduced. The underlying logic of this framework allows us to build a simulation engine for executing system specifications. This engine makes intensive use of automated theorem proving – when running a simulation, almost all computational steps are those of a theorem prover. In this paper, we present this novel combination of a logical setting involving meta-level logics and large sets of formulae for system description, together with theorem proving requirements which involve often slowly changing specifications with the need for rapid assessment of deducibility and consistency. We will evaluate the suitability of several theorem provers for this application.

15:55 Han-Hing Dang and Peter Höfner
Automated Higher-order Reasoning in Quantales

Originally developed as an algebraic characterisation for quantum mechanics, the algebraic structure of quantales nowadays finds widespread applications ranging from (non-commutative) logics to hybrid systems. We present an approach to bring reasoning in quantales into the realm of (fully) automated theorem proving. Hence the paper paves the way for automatisation in various (new) fields of applications. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Problem Library for higher-order logic. In particular, we give an encoding of quantales in the typed higher-order form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.

16:20 Jens Otten and Geoff Sutcliffe
Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi

The TPTP language, developed within the framework of the TPTP library, allows the representation of problems and solutions in first-order and higher-order logic. Whereas the writing of solutions in resolution calculi is well documented and used, an appropriate representation of solutions in tableau or connection calculi using the TPTP syntax is not specified so far. This paper describes how the TPTP language can be used to represent derivations and solutions in tableau and connection calculi.

16:45 Christoph Benzmueller and Adam Pease
Progress in Automating Higher-Order Ontology Reasoning

We report on the application of higher-order automated theorem proving in ontology reasoning. Concretely, we have integrated the Sigma knowledge engineering environment and the Suggested Upper-Level Ontology SUMO with the higher-order theorem prover LEO-II. The basis for this integration is a translation from SUMO representations into the new typed higher-order form representation language TPTP THF. We illustrate the benefits of our integration with examples, report on experiments and analyze open challenges.

17:10 Ullrich Hustadt and Renate A. Schmidt
A Comparison of Solvers for Propositional Dynamic Logic

Calculi for propositional dynamic logics have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical procedures been suggested and implemented. In this paper, we compare three such systems, namely, the Tableau Workbench by Abate, Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009).