6th Workshop on practical aspects of automated reasoning

PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop will bring together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It will allow researchers to present their work in progress, and to discuss new implementation techniques and applications.

Accepted papers

Ahmed Bhayat (The University of Manchester)
Giles Reger (The University of Manchester)
Set of Support for Higher-Order Reasoning

ABSTRACT. Higher-order logic (HOL) is utilised in numerous domains from program verification to the formalisation of mathematics. However, automated reasoning in the higher-order domain lags behind first-order automation. Many higher-order automated provers translate portions of HOL problems to first-order logic (FOL) and pass them to FOL provers. However, FOL provers are not optimised for dealing with these translations. One of the reasons for this is that the axioms introduced during the translation (e.g. those defining combinators) may combine with each during proof search, deriving consequences of the axioms irrelevant to the goal. In this work we evaluate the extent to which this issue affects proof search and introduce heuristics based on the set-of-support strategy for minimising the effects. Our experiments are carried out within the Vampire theorem prover and show that limiting how axioms introduced during translation can improve proof search with higher-order problems.

Gabriel Ebner (Vienna University of Technology)
Matthias Schlaipfer (Vienna University of Technology)
Efficient translation of sequent calculus proofs into natural deduction proofs

ABSTRACT. We present a simple and efficient translation of the classical multi-succedent sequent calculus LK to natural deduction. This translation aims to produce few excluded middle inferences, and to keep the quantifier complexity of the instances of excluded middle low. We evaluate the translation on proofs imported from resolution-based first-order theorem provers, and show that it achieves these goals in an efficient manner.

Ullrich Hustadt (University of Liverpool)
Cláudia Nalon (University of Brasília)
Clare Dixon (University of Liverpool)
Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics

ABSTRACT. We consider the transformation of propositional linear time temporal logic formulae into a clause normal form, called Separated Normal Form, suitable for resolution calculi. In particular, we investigate the effect of applying various pre-processing techniques on characteristics of the normal form and determine the best combination of techniques on a large collection of benchmark formulae.

Jens Otten (University of Oslo)
Proof Search Optimizations for Non-clausal Connection Calculi

ABSTRACT. The paper presents several proof search optimization techniques for non-clausal connection calculi. These techniques are implemented and integrated into the non-clausal connection prover nanoCoP. Their effectiveness is evaluated on the problems in the TPTP library. Together with a fixed strategy scheduling, these techniques are the basis of the new version 1.1 of nanoCoP.

Michael Rawson (The University of Manchester)
Giles Reger (The University of Manchester)
Dynamic Strategy Priority: Empower the strong and abandon the weak

ABSTRACT. Automated theorem provers are often used in other tools as black-boxes for discharging proof obligations. One example where this has enjoyed a lot of success is within interactive theorem proving. A key usability factor in such settings is the time taken for the provers to complete. Automated theorem provers run lists of proof strategies sequentially, which can cause proofs to be found more slowly than necessary. We show that it is possible to predict which strategies are likely to succeed while they are running using an artificial neural network. We also implement a run-time strategy scheduler in the Vampire theorem prover which improves average proof search time, and hence increases usability as a black-box solver.

Geoff Sutcliffe (University of Miami)
Evgenii Kotelnikov (Chalmers University of Technology)
TFX: The TPTP Extended Typed First-order Form

ABSTRACT. The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving systems for classical logics. The TPTP language is one of the keys to the success of the TPTP world. Originally the TPTP world supported only first-order clause normal form (CNF). Over the years support for full first-order form (FOF), monomorphic typed first-order form (TF0), rank-1 polymorphic typed first-order form (TF1), monomorphic typed higher-order form (TH0), and rank-1 polymorphic typed higher-order form (TH1), have been added. TF0 and TF1 together form the TFF language family; TH0 and TH1 together form the THF language family. This paper introduces the eXtended Typed First-order form (TFX), which extends TFF to include boolean terms, tuples, conditional expressions, and let expressions.

Jørgen Villadsen (Technical University of Denmark)
Anders Schlichtkrull (Technical University of Denmark)
Andreas Halkjær From (Technical University of Denmark)
A Verified Simple Prover for First-Order Logic

ABSTRACT. We present a simple prover for first-order logic with certified soundness and completeness in Isabelle/HOL, taking formalizations by Tom Ridge and others as the starting point, but with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level. The prover is simple in the following sense: It is purely functional and can be executed with rewriting rules or as code generation to a number of functional programming languages. The prover uses no higher-order functions, that is, no function takes a function as argument or returns a function as its result. This is advantageous when students perform rewriting steps by hand. The prover uses the logic of first-order logic on negation normal form with a term language consisting of only variables. This subset of the full syntax of first-order logic allows for a simple proof system without resorting to the much weaker propositional logic.

Programme Committee

Invited Speakers

  • Magnus O. Myreen: The CakeML Verified Compiler and Toolchain 


PAAR proceedings will be published electronically in the CEUR workshop proceedings.


Oxford, UK