Exceptions in the rewriting calculus

Germain Faure 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/inria-00101011
Contributor : Germain Faure <>
Submitted on : Monday, September 18, 2006 - 9:43:01 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM
Long-term archiving on : Monday, April 5, 2010 - 10:53:13 PM

Identifiers

  • HAL Id : inria-00101011, version 2

Collections

Citation

Germain Faure, Claude Kirchner. Exceptions in the rewriting calculus. 13th International Conference on Rewriting Techniques and Applications - RTA 2002, Jul 2002, Copenhagen/Denmark, pp.66--82. ⟨inria-00101011v2⟩

Share

Metrics

Record views

195

Files downloads

92