zbMATH — the first resource for mathematics

On a generalised logicality theorem. (English) Zbl 1072.68536
Calmet, Jacques (ed.) et al., Artificial intelligence, automated reasoning, and symbolic computation. Joint international conferences: AISC 2002, the 6th international conference on artificial intelligence and symbolic computation, and Calculemus 2002, the 10th symposium on the integration of symbolic computation and mechanized reasoning. Marseille, France, July 1–5, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43865-3). Lect. Notes Comput. Sci. 2385, 51-63 (2002).
Summary: In this paper, the correspondence between derivability (syntactic consequences obtained from \( \vdash\)) and convertibility in rewriting \(( {\overset{*}{\leftrightarrow}}\)), 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 \( \vdash\) of the logic under consideration.
For the entire collection see [Zbl 0993.00048].

68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03F07 Structure of proofs
Full Text: Link