Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Theorem Proving Modulo Revised Version

Gilles Dowek 1 Thérèse Hardin 2 Claude Kirchner 3 
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
3 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits to separate computations and deductions in a clean way. The first contribution of this paper is to define a sequent calculus modulo that gives a proof theoretic account of the combination of computations and deductions. The congruence on propositions is handled via rewrite rules and equational axioms. Rewrite rules apply to terms but also directly to atomic propositions. The second contribution is to give a complete proof search method, called Extended Narrowing and Resolution (ENAR), for theorem proving modulo such congruences. The completeness of this method is proved with respect to provability in sequent calculus modulo. An important application is that higher-order logic can be presented as a theory in deduction modulo. Applying the Extended Narrowing and Resolution method to this presentation of higher-order logic subsumes full higher-order resolution.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 6:36:30 PM
Last modification on : Wednesday, October 26, 2022 - 8:15:59 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:35:02 PM


  • HAL Id : inria-00071722, version 1


Gilles Dowek, Thérèse Hardin, Claude Kirchner. Theorem Proving Modulo Revised Version. [Research Report] RR-4861, INRIA. 2003, pp.54. ⟨inria-00071722⟩



Record views


Files downloads