IJCAR '08 Workshop on Practical Aspects of Automated Reasoning (PAAR-2008)

Skyline of Sydney, courtesy of Matthew Field via the Wikimedia
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:

We are particularly interested in contributions that help the community to understand how to build useful and powerful 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.

Submission is now closed, see the bottom of the page for the published proceedings.

Final versions

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.

Important dates:


Invited Speakers

Higher-Order System Demonstration

A demonstration of the practical use of higher-order resoning systems is planned for August 10th.

Full Schedule

Sunday, August 10

 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
 15.10 Stefan Berghofer
 15.20 Lucas Dixon
 15.30-16.00 Coffee break
 16.00-17.20 ESHOL System demonstration (Introduction, continued)
 16.00 Guillaume Melquiond
 16.10 Josef Urban
 16.20 Joe Hurd
 16.30 Carsten Schürmann
 16.40 Christoph Benzmüller and Frank Theiss
 16.50 Christoph Benzmüller and Frank Theiss
 17.00 Mark Kaminski
 17.15- ESHOL System demonstration (Practical demonstrations)
   Running in parallel

Monday, August 11

 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

Workshop Proceedings

The workshop proceedings are now available as Volume 373 of the CEUR Workshop Proceedings.

AI Communications

We are preparing a special issue on Practical Aspects of Automated Reasoning for the Journal of AI Communications. See the Call for Papers.