|
 
|
[Bur11b] Experimenting with deduction modulo
Conférence Internationale avec comité de lecture : 23rd International Conference on Automated Deduction, July 2011, Vol. 6803, pp.162--176, Series LNAI, Wroclaw, Poland, (DOI: 10.1007/978-3-642-22438-6_14)Mots clés: proving modulo theory,ordered resolution,rewriting,implementation,first-order theorem prover
Résumé:
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 have given 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 with other proof-search calculi, using benchmarks extracted from the TPTP Library. We also compare several implementation techniques for the integration of rewriting, some being based on discrimination trees, some being based on compilation. These results reveal that deduction modulo is a promising approach to handle proof search in theories in a generic but efficient way.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| Bur11b, | |||
| title | = | "{Experimenting with deduction modulo}", | |
| author | = | " G. Burel ", | |
| booktitle | = | "{23rd International Conference on Automated Deduction}", | |
| year | = | 2011, | |
| edition | = | "Springer", | |
| month | = | "July", | |
| series | = | "LNAI", | |
| volume | = | 6803, | |
| pages | = | "162--176", | |
| address | = | "Wroclaw, Poland", | |
| doi | = | "10.1007/978-3-642-22438-6_14", | |
| } | |||
