Image courtesy of Matthew Field via the Wikimedia Commons.
Image courtesy of Matthew Field via the Wikimedia Commons.
The first Workshop on Practical Aspects of Automated Reasoning will be held in August 2008, in Sydney, Australia. PAAR will be associated with the 4th International Joint Conference on Automated Reasoning (IJCAR-2008).
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.
Submission is now closed, see the bottom of the page for the published proceedings.
The final versions should be prepared in LaTeX using the Springer Verlag llncs class. The workshop proceedings have now been published as CEUR Workshop Proceedings and were available at the event.
We plan to produce a special issue of a recognized journal on the topic of the workshop.
Abstract: Software Model Checking is emerging as one of the leading approaches to automatic program analysis. State-of-the-art software model checkers exhibit levels of automation and precision often superior to those provided by traditional software analysis tools. This success is due to a large extent to the use of Satisfiability Modulo Theory (SMT) solvers to support reasoning about complex and even infinite data structures (e.g. bit-vectors, numeric data, arrays) manipulated by the program being analysed. In this talk I will survey the opportunities and challenges posed to Automated Reasoning by this new application domain.
Abstract: Specification and verification in continuous problem domains are key topics for the practical application of formal methods and mechanized reasoning. The mathematics in these problem domains is intrinsically higher-order: even the simplest theorems involve quantification over sets and functions. I will discuss one approach to linear continuous control systems and consider the challenges and opportunities raised for mechanized reasoning. These include practical implementation and integration issues, algorithms in computational real algebraic geometry and hard open questions such as the Schanuel conjecture.
Abstract: The process of modelling a problem in a form suitable for solution by constraint satisfaction or operations research techniques, as opposed to the process of solving it once formulated, requires a significant amount of reasoning. Contemporary modelling languages separate the first order description or "model" from its grounding instantiation or "data". Properties of the model independent of the data may thus be established by first order reasoning. In this talk, I survey the opportunities arising from this new application direction for automated deduction, and note some of the formidable obstacles in the way of a practically useful implementation.
A demonstration of the practical use of higher-order resoning systems is planned for August 10th.
| 09.00-10.00 | Invited talk: Alessandro Armando (shared with CEDAR) | |
|---|---|---|
| Software Model Checking: new challenges and opportunities for Automated Reasoning | ||
| 10.00-10.30 | Coffee break | |
| 10.30-12.30 | Session 1 | |
| 10.30 | Joao Marcos and Dalmo Mendonca | |
| Towards fully automated axiom extraction for finite-valued logics | ||
| 11.10 | Paulo Pinheiro da Silva, Geoff Sutcliffe, Cynthia Chang, Li Ding, Nick del Rio and Deborah McGuinness | |
| Presenting TSTP Proofs with Inference Web Tools | ||
| 11.50 | Steven Trac, Geoff Sutcliffe and Adam Pease | |
| Integration of the TPTPWorld into SigmaKEE | ||
| 12.30-14.00 | Lunch break | |
| 14.00-15.00 | ESHOL invited talk: Rob Arthan | |
| Mechanized Reasoning for Continuous Problem Domains | ||
| 15.00-15.30 | ESHOL System demonstration (Introduction) | |
| 15.00 | Rob Arthan | |
| ProofPower | ||
| 15.10 | Stefan Berghofer | |
| Isabelle | ||
| 15.20 | Lucas Dixon | |
| IsaPlanner | ||
| 15.30-16.00 | Coffee break | |
| 16.00-17.20 | ESHOL System demonstration (Introduction, continued) | |
| 16.00 | Guillaume Melquiond | |
| Coq | ||
| 16.10 | Josef Urban | |
| Mizar | ||
| 16.20 | Joe Hurd | |
| HOL | ||
| 16.30 | Carsten Schürmann | |
| Delphin | ||
| 16.40 | Christoph Benzmüller and Frank Theiss | |
| Omega | ||
| 16.50 | Christoph Benzmüller and Frank Theiss | |
| LEO II | ||
| 17.00 | Mark Kaminski | |
| TPS | ||
| 17.15- | ESHOL System demonstration (Practical demonstrations) | |
| Running in parallel |
| 09.00-10.00 | Invited talk: John Slaney | |
|---|---|---|
| Constraint Modelling: A Challenge for First Order Automated Reasoning | ||
| 10.00-10.30 | Coffee break | |
| 10.30-12.30 | Session 2 | |
| 10.30 | Christoph Weidenbach and Patrick Wischnewski | |
| Contextual Rewriting in SPASS | ||
| 11.10 | Nachum Dershowitz | |
| Bit Inference | ||
| 11.50 | Hans de Nivelle and Piotr Witkowski | |
| A Small Framework for Proof Checking | ||
| 12.30-14.00 | Lunch break | |
| 14.00-15.30 | Session 3 | |
| 14.00 | Timothy Hinrichs | |
| Collaborative Programming: Applications of logic and automated reasoning | ||
| 14.40 | Björn Pelzer and Ingo Glöckner | |
| Combining Theorem Proving with Natural Language Processing | ||
| 15.30-16.00 | Coffee break | |
| 16.00-17.10 | Session 4 | |
| 16.00 | Adam Pease, Geoff Sutcliffe, Nick Siegel and Steven Trac | |
| The Annual SUMO Reasoning Prizes at CASC | ||
| 16.40 | Thomas Raths and Jens Otten | |
| randoCoP: Randomizing the Proof Search Order in the Connection Calculus | ||
| 17.20-18.00 | ESHOL panel: Rob Arthan, Lucas Dixon, Joe Hurd | |
| Evaluation of Systems for Higher Order Logic |
