Exceptions in the rewriting calculus
| Autor: | Claude Kirchner, Germain Faure |
|---|---|
| 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), Sophie Tison |
| Jazyk: | angličtina |
| Rok vydání: | 2002 |
| Předmět: |
Discrete mathematics
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Programming language Semantics (computer science) 020207 software engineering Context (language use) 0102 computer and information sciences 02 engineering and technology 16. Peace & justice computer.software_genre 01 natural sciences Expression (mathematics) Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Simple (abstract algebra) Confluence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Rewriting Lambda calculus computer computer.programming_language Mathematics |
| Zdroj: | 13th International Conference on Rewriting Techniques and Applications-RTA 2002 13th International Conference on Rewriting Techniques and Applications-RTA 2002, Jul 2002, Copenhagen/Denmark, pp.66--82 Rewriting Techniques and Applications ISBN: 9783540439165 RTA |
| Popis: | In the context of the rewriting calculus, we introduce and study an exception mechanism that allows us to express in a simple way rewriting strategies and that is therefore also useful for expressing theorem proving tactics. The proposed exception mechanism is expressed in a confluent calculus which gives the ability to simply express the semantics of the first tactical and to describe in full details the expression of conditional rewriting. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|