Page de Guillaume BUREL (photo de Guillaume Burel)

iProver Modulo

In [1] we have shown that it is sound and complete to integrate Deduction Modulo into a prover, and that it is rather easy if the prover is based on the given-clause algorithm. In [2] we detail the implementation of these ideas into the prover iProver developed by Konstantin Korovin at the University of Manchester, and we give the results of benchmarks using problems of the TPTP Library.

The source code of our implementation is available as a patch to iProver v0.7. We also provide the input files describing the rewrite systems that were used in the benchmarks of [2].

Since version 0.7+0.2 of the patch, iProver modulo is able to output proofs in the Dedukti format. See [3] for details about this embedding.

References

[1] Guillaume Burel. Embedding deduction modulo into a prover. In Anuj Dawar and Helmut Veith (eds.), CSL, volume 6247 of LNCS, pages 155-169. Springer, 2010. .pdf  .bib  ©Springer.Abstract Deduction modulo consists in presenting a theory through rewrite rules to support automatic and interactive proof search. It induces proof search methods based on narrowing, such as the polarized resolution modulo. We show how to combine this method with more traditional ordering restrictions. Interestingly, no compatibility between the rewriting and the ordering is requested to ensure completeness. We also show that some simplification rules, such as strict subsumption eliminations and demodulations, preserve completeness. For this purpose, we use a new framework based on a proof ordering. These results show that polarized resolution modulo can be integrated into existing provers, where these restrictions and simplifications are present. We also discuss how this integration can actually be done by diverting the main algorithm of state-of-the-art provers.

[2]Guillaume Burel. Experimenting with deduction modulo. In Viorica Sofronie-Stokkermans and Nikolaj Bjørner (eds.), CADE 2011, volume 6803 of LNAI, pages 162-176. Springer, 2011. .pdf  .bib  ©Springer.Abstract Deduction modulo is a generic framework to describe proofs in a theory better than using raw axioms. This is done by presenting the theory through rules rewriting terms and propositions. In CSL 2010, LNCS 6247, p.155-169, we gave theoretical justifications why it is possible to embed a proof search method based on deduction modulo, namely Ordered Polarized Resolution Modulo, into an existing prover. Here, we describe the implementation of these ideas, starting from iProver. We test it by confronting Ordered Polarized Resolution Modulo and other proof-search calculi, using benchmarks extracted from the TPTP Library. For the integration of rewriting, we also compare several implementation techniques, based for instance on discrimination trees or on compilation. These results reveal that deduction modulo is a promising approach to handle proof search in theories in a generic but efficient way.

[3]Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the lamdba-Pi-Calculus Modulo, submitted.  .pdf