The LPAR 2008 Workshop on

Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA)

will be held on November 22, 2008 preceding

The 15th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning
November 23-27, 2008, Doha, Qatar

Why?

We believe that existing automated provers and proof assistants are complementary, to the point that their cooperative integration would benefit all efforts in automating reasoning. Indeed, a number of specialized tools incorporating such integration have been built. The issue is, however, wider, as we can envisage cooperation among various automated provers as well as among various proof assistants.

This workshop will bring together practitioners and researchers who have experimented with knowledge exchange among tools supporting automated reasoning. Relatively little stress will be put on ideas that are not yet implemented but such contributions are also welcome.

Topics of interests

  • Formats for knowledge exchange.
  • Delegating tasks from proof assistants to theorem provers.
  • Interfacing to more than one theorem prover.
  • Imports from theorem provers that can be trusted.
  • Sharing libraries among proof assistants.

Organizers

  • Piotr Rudnicki, University of Alberta (Canada)
  • Geoff Sutcliffe, University of Miami (USA)

Programme Committee

  • Andrea Asperti, University of Bologna (Italy)
  • Christoph Benzmüller, Saarland University (Germany)
  • William M. Farmer, McMaster University (Canada)
  • Joe Hurd, Galois, Inc. (USA)
  • John Matthews, Galois, Inc. and Portland State University (USA)
  • Tobias Nipkow, Technical University Munich (Germany)
  • Michael Norrish, NICTA (Australia)
  • Piotr Rudnicki, University of Alberta (Canada)
  • Christoph Schwarzweller, University of Gdansk (Poland)
  • Geoff Sutcliffe, University of Miami (USA)
  • Josef Urban, Charles University (Czech Republic)
  • Freek Wiedijk, Radboud University Nijmegen (The Netherlands)

Invited Speaker

Josef Urban, Exporting from the Mizar Library

Submission

Please submit an extended abstract of up to 10 pages in PDF, conforming to the format produced by LaTeX using the easychair.cls class file. Long listings of computer output should be relegated to a referenced WWW site. Submission is via EasyChair (thanks to Andrei Voronkov). All submissions will be informally reviewed by the programme committee and accepted contributions will be published in archived electronic notes.

Proposals for system and application demonstrations at the workshop are also invited.

Submission deadline: October 18, 2008
Notification of acceptance: October 27, 2008
Workshop: November 22, 2008

If you have any questions, please email to keappa08@cs.ualberta.ca