Workshop on Practical Aspects of Automated Reasoning (PAAR-2010)

Arthur's Seat, Edinburgh, Scottland. From the Wikimedia

The Second Workshop on Practical Aspects of Automated Reasoning will be held in July 2010, in Edinburgh, UK. PAAR will be part of FLoC 2010 and associated with the 5th International Joint Conference on Automated Reasoning (IJCAR-2010).

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. This 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.

Topics include but are not limited to:

We are particularly interested in contributions that help the community to understand how to build useful reasoning systems in practice, and how to apply existing systems to real problems.

Program committee


Researchers interested in participating are invited to submit a short (2-10 pages) abstract via EasyChair. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions.

Submissions should be in standard-conforming Postscript or PDF.

To submit a paper, go to the EasyChair PAAR page and follow the instructions there.

You can view the full call for papers.

Final versions

Final versions should be prepared in LaTeX using the easychair.cls class file. Proceedings will be published as EasyChair or CEUR Workshop Proceedings and will be available in print at the event.

If number and quality of the submissions warrant are sufficient, we plan to produce a special issue of a recognized journal on the topic of the workshop.

Important dates:

All dates are preliminary and may change according to FLoC requirements.


A preliminary version of the proceedings (~4 MB PDF) is now available.


Contributed talks in the morning are 30 minutes long, contributed talks in the afternoon are 25 minutes. It's the luck of the draw. Please allow at least 5 minutes of your time slot for discussion.
PAAR-2010, Wednesday, 14 July 2010
9:00 - 10.00Invited talk: Lawrence C. Paulson and Jasmin Christian Blanchette
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:00 - 10:30Coffee break
10:30 - 11:00Laura Meikle and Jacques Fleuriot
Automation for Geometry in Interactive Theorem Provers
11:00 - 11:30Andrew Matusiwicz, Neil Murray and Erik Rosenthal
Trie Based Subsumption and Improving the pi-Trie Algorithm
11:30 - 12:00Guido Fiorino
Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus
12:00 - 12:30Thomas Bouton, Diego Caminha, David Deharbe and Pascal Fontaine
GridTPT: a distributed platform for Theorem Prover Testing
12:30 - 14:00Lunch break
14:00 - 15.00Invited talk: Andrei Voronkov
Vampire: the New 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:00 - 15:30Coffee break
15:30 - 15:55Djihed Afifi, David Rydeheard and Howard Barringer
Automated Reasoning in the Simulation of Evolvable Systems
15:55 - 16:20Han-Hing Dang and Peter Höfner
Automated Higher-order Reasoning in Quantales
16:20 - 16:45Jens Otten and Geoff Sutcliffe
Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi
16:45 - 17:10Christoph Benzmueller and Adam Pease
Progress in Automating Higher-Order Ontology Reasoning
17:10 - 17:35 Ullrich Hustadt and Renate A. Schmidt
A Comparison of Solvers for Propositional Dynamic Logic
17:35The End

Previous Event