Exceptions in the rewriting calculus

被引：0

作者：

Faure, G

Kirchner, C

机构：

[1] Ecole Normale Super Lyon, F-69364 Lyon 07, France

[2] LORIA, F-69364 Lyon, France

[3] LORIA, F-54602 Villers Les Nancy, France

[4] INRIA, F-54602 Villers Les Nancy, France

来源：

REWRITING TECHNIQUES AND APPLICATIONS | 2002年 / 2378卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：66 / 82

页数：17

共 12 条

[1]

BOROVANSKY P, 1998, ELECT NOTES THEORETI

[2]

BOULTON R, 1992, IFIP TRANS A, V10, P129

[3]

Cirstea H., 2001, LECT NOTES COMPUTER, P166

[4]

CIRSTEA H, 2001, LOG J IGPL, V9, P427, DOI DOI 10.1093/JIGPAL/9.3.339

[5]

CIRSTEA H, 2000, THESIS U H POINCARE

[6]

CIRSTEA H, 2001, LECT NOTES COMPUTER, V2051

[7] A RATIONALE FOR CONDITIONAL EQUATIONAL PROGRAMMING [J].

DERSHOWITZ, N ;

OKADA, M .

THEORETICAL COMPUTER SCIENCE, 1990, 75 (1-2) :111-138

[8]

DUBOIS H, 2000, P 2 AMAST WORKSH ALG

[9]

FAURE G, 2001, ETUDE PROPRIETES CAL

[10] THEORY OF TYPE POLYMORPHISM IN PROGRAMMING [J].

MILNER, R .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1978, 17 (03) :348-375

← 1 2 →