Proof theory for reasoning with Euler diagrams : a Logic Translation and Normalization
Proof theory for reasoning with Euler diagrams : a Logic Translation and Normalization
复制标题
用欧拉图推理的证明理论：逻辑转换和规范化
DOI：
10.1007/s11225-012-9370-6
复制
发表时间：
2012
期刊：
影响因子：
0.7
通讯作者：
Ryo Takemura
中科院分区：
文献类型：
--
作者：
Nakanishi;H.;Ryo Takemura
在形式证明的句子/符号表示的基础上开发的证明理论概念和技术应用于欧拉图。给出了欧拉图解系统到自然演绎系统的翻译，并证明了翻译的合理性和忠实性。翻译的一些后果是根据搭便车的概念来讨论的，搭便车的概念主要在认知科学文献中作为图表推理功效的说明进行讨论。该翻译使我们能够根据证明理论对搭便车进行形式化和分析。研究了欧拉图解证明的范式概念，并证明了归一化定理。进一步讨论了该定理的一些后果：特别是对正常图解证明的结构的分析；通常子公式属性的图形对应项；以及图解证明与自然演绎证明相比的特征。
Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us to formalize and analyze free ride in terms of proof theory. The notion of normal form of Euler diagrammatic proofs is investigated, and a normalization theorem is proved. Some consequences of the theorem are further discussed: in particular, an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; and a characterization of diagrammatic proofs compared with natural deduction proofs.