Counter-Example Construction with Euler Diagrams
Counter-Example Construction with Euler Diagrams
复制标题
DOI：
10.1007/s11225-014-9584-x
复制
发表时间：
2014-10
期刊：
影响因子：
0.7
通讯作者：
Ryo Takemura
中科院分区：
文献类型：
--
作者：
Ryo Takemura
欧拉图的传统应用之一是作为给定句子的通常集合理论模型的表示或对应物。然而，欧拉图最近被研究作为对应的逻辑公式，构成形式证明。欧拉图被严格定义为语法对象，其推理系统被形式化，等价于某些符号逻辑系统。基于这一观察，我们调查的反模型建设和证明建设的框架下的欧拉图。我们引入了“反图解证明”的概念，这表明了一个给定的推理的无效性，并被定义为一个语法操作的图相同的排序推理规则，以构建证明。因此，在我们的欧拉图解框架中，完备性定理可以用图解证明或反图解证明的存在性来形式化。
One of the traditional applications of Euler diagrams is as a representation or counterpart of the usual set-theoretical models of given sentences. However, Euler diagrams have recently been investigated as the counterparts of logical formulas, which constitute formal proofs. Euler diagrams are rigorously defined as syntactic objects, and their inference systems, which are equivalent to some symbolic logical systems, are formalized. Based on this observation, we investigate both counter-model construction and proof-construction in the framework of Euler diagrams. We introduce the notion of “counter-diagrammatic proof”, which shows the invalidity of a given inference, and which is defined as a syntactic manipulation of diagrams of the same sort as inference rules to construct proofs. Thus, in our Euler diagrammatic framework, the completeness theorem can be formalized in terms of the existence of a diagrammatic proof or a counter-diagrammatic proof.