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:
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 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.
| PAAR-2010, Wednesday, 14 July 2010 | ||
| 9:00 - 10.00 | Invited 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:30 | Coffee break | |
| 10:30 - 11:00 | Laura Meikle and Jacques Fleuriot | |
| Automation for Geometry in Interactive Theorem Provers | ||
| 11:00 - 11:30 | Andrew Matusiwicz, Neil Murray and Erik Rosenthal | |
| Trie Based Subsumption and Improving the pi-Trie Algorithm | ||
| 11:30 - 12:00 | Guido Fiorino | |
| Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus | ||
| 12:00 - 12:30 | Thomas Bouton, Diego Caminha, David Deharbe and Pascal Fontaine | |
| GridTPT: a distributed platform for Theorem Prover Testing | ||
| 12:30 - 14:00 | Lunch break | |
| 14:00 - 15.00 | Invited 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:30 | Coffee break | |
| 15:30 - 15:55 | Djihed Afifi, David Rydeheard and Howard Barringer | |
| Automated Reasoning in the Simulation of Evolvable Systems | ||
| 15:55 - 16:20 | Han-Hing Dang and Peter Höfner | |
| Automated Higher-order Reasoning in Quantales | ||
| 16:20 - 16:45 | Jens Otten and Geoff Sutcliffe | |
| Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi | ||
| 16:45 - 17:10 | Christoph 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:35 | The End |