Certifying Term Rewriting Proof in ELAN
| Autor: | Nguyen, Quang-Huy |
|---|---|
| Přispěvatelé: | Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, 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) |
| Jazyk: | angličtina |
| Rok vydání: | 2001 |
| Předmět: |
proof checking
proof term of term rewriting terme de preuve de la réécriture TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science term rewriting modulo ac ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] Computer Science::Programming Languages la réécriture modulo ac Computer Science::Symbolic Computation vérification de preuve |
| Zdroj: | 2nd International Workshop on Rule-based Programming-RULE'01 2nd International Workshop on Rule-based Programming-RULE'01, Sep 2001, Firenze, Italy, 18 p |
| Popis: | Colloque avec actes et comité de lecture. internationale.; International audience; Term rewriting has been shown to be a good environment for both programming and proving. We consider the proof term of term rewriting and propose a formalism based on the rewriting calculus with explicit substitutions ($\rho\sigma$-calculus). This formalism is helpful in analysing and in debugging rule-based programs. Moreover, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic term rewriting but also with term rewriting modulo a set of axioms ({\em e.g.} associativity-commutativity). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|