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.
This work was begun while the author was a post-doc fellow at the Max-Planck-Institute for Informatics in Saarbrüken, Germany.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J.: λυ, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming 6(5), 699–722 (1996)
Berger, U., Eberl, M., Schwichtenberg, H.: Normalization by evaluation. In: Möller, B., Tucker, J.V. (eds.) NADA 1997. LNCS, vol. 1546, pp. 117–137. Springer, Heidelberg (1998)
Bonichon, R., Hermant, O.: A semantic completeness proof for taMeD. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 167–181. Springer, Heidelberg (2006)
Burel, G.: Embedding deduction modulo into a prover. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 155–169. Springer, Heidelberg (2010)
Burel, G.: Efficiently simulating higher-order arithmetic by a first-order theory modulo. Logical Methods in Computer Science 7(1:3), 1–31 (2011)
Burel, G., Kirchner, C.: Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation 208(2), 140–164 (2010)
Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007)
Dowek, G.: Polarized resolution modulo. In: Calude, C.S., Sassone, V. (eds.) IFIP TCS. IFIP AICT., vol. 323, pp. 182–196. Springer, Heidelberg (2010)
Dowek, G., Hardin, T., Kirchner, C.: HOL-λσ. Mathematical Structures in Computer Science 11(1), 1–25 (2001)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)
Dowek, G., Miquel, A.: Cut elimination for Zermelo’s set theory (2006); available on authors’ web page
Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 423–437. Springer, Heidelberg (2005)
Graf, P. (ed.): Term Indexing. LNCS (LNAI), vol. 1053. Springer, Heidelberg (1996)
Korovin, K.: iProver – an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)
Razianov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)
Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004)
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009)
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE. LNCS, vol. 5663, pp. 140–145. Springer (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Burel, G. (2011). Experimenting with Deduction Modulo. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-22438-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22437-9
Online ISBN: 978-3-642-22438-6
eBook Packages: Computer ScienceComputer Science (R0)