Abstract | ||
---|---|---|
In this paper, the correspondence between derivability (syntactic consequences obtained from 驴) and convertibility in rewriting (驴), the so-called logicality, is studied in a generic way (i.e. logic-independent). This is achieved by giving simple conditions to characterise logics where (bidirectional) rewriting can be applied. These conditions are based on a property defined on proof trees, that we call semi-commutation. Then, we show that the convertibility relation obtained via semi-commutation is equivalent to the inference relation 驴 of the logic under consideration. |
Year | DOI | Venue |
---|---|---|
2002 | 10.1007/3-540-45470-5_8 | AISC |
Keywords | Field | DocType |
generalised logicality theorem,convertibility relation,inference relation,syntactic consequence,proof tree,simple condition,so-called logicality,computer algebra | Discrete mathematics,Formal system,Computer science,Inference,Symbolic computation,Theoretical computer science,Rewriting,Convertibility,Syntax | Conference |
ISBN | Citations | PageRank |
3-540-43865-3 | 5 | 0.42 |
References | Authors | |
8 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Marc Aiguier | 1 | 98 | 14.95 |
Diane Bahrami | 2 | 10 | 1.89 |
Catherine Dubois | 3 | 24 | 7.06 |