[FOM] KEAPPA - knowledge exchange for automated reasoning

Geoff Sutcliffe by way of Martin Davis <martin@eipye.com> geoff at cs.miami.edu
Sat Sep 13 12:48:30 EDT 2008

Dear Martin,

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. We have therefore arranged the following
workshop, and invite you to submit. We hope to see you in Qattar!


Piotr and Geoff


                      KEAPPA Workshop - 22nd November 2008

           Knowledge Exchange: Automated Provers and Proof Assistants


        preceding LPAR'08, the 15th International Conference on Logic for
              Programming, Artificial Intelligence and Reasoning
          November 23-27, 2008, Carnegie Mellon University, Doha, Qatar

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.

Please submit an extended abstract of up to 10 pages, following the
instructions in the KEAPPA web site ...

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

Invited Speaker
+ Josef Urban, Exporting from the Mizar Library

More information about the FOM mailing list