Theorem Proving Modulo
In: https://inria.hal.science/inria-00077199 ; [Research Report] RR-3400, INRIA. 1998, pp.27, 1998
Online
report
Zugriff:
Projet COQ, Projet PARA, PROTHEO ; «Theorem proving 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 wider interest because it aims at separating deductions and computations. The first contribution of this paper is to provide a «sequent calculus modulo» that gives a clear distinction between the decidable (computation) and the undecidable (deduction). The congruence on propositions is handled via rewrite rules and equational axioms. Usually rewriting applies only to terms. The second contribution of this paper is to allow rewriting atomic propositions into non atomic ones and to give a complete proof search method, called «Extended Narrowing and Resolution» (ENAR), modulo such congruences. The completeness of this method is proved using the sequent calculus modulo. An important application is that this Extended Narrowing and Resolution method subsumes full higher-order resolution when applied to a first-order presentation of higher-order logic. This shows that such a presentation can yield also efficient proof-search methods.
Titel: |
Theorem Proving Modulo
|
---|---|
Autor/in / Beteiligte Person: | Dowek, Gilles ; Hardin, Thérèse ; Kirchner, Claude ; Rocquencourt, INRIA ; Institut National de Recherche en Informatique et en Automatique (Inria) ; Sémantiques, preuves et implantation (SPI) ; Laboratoire d'Informatique de Paris 6 (LIP6) ; Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS) ; Constraintsomatic deduction and software properties proofs (PROTHEO) ; Lorraine, INRIA ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS) ; INRIA |
Link: | |
Zeitschrift: | https://inria.hal.science/inria-00077199 ; [Research Report] RR-3400, INRIA. 1998, pp.27, 1998 |
Veröffentlichung: | HAL CCSD, 1998 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|