【作者】 李巍；

【导师】 李娜；

【作者基本信息】 南开大学 ， 逻辑学， 2014， 博士

【摘要】 核证的概念自柏拉图时代以来就是认知研究中的一个重要部分,柏拉图对知识有三个准则：核证,真,信念,但是,尽管逻辑研究者在知识和信念的形式化的逻辑模型中处理了信念和真,核证却一直缺少相应的处理,直到核证逻辑出现后,核证才被引入到知识的逻辑模型中。哥德尔在1938年就对核证逻辑有所论述,阿尔捷莫夫和施特拉森提出了证明逻辑的雏形,阿尔捷莫夫在1994年首次给出了证明逻辑LP,在2001年完全正式地、比较系统地给出了证明逻辑LP,由此可以引出许多新的核证逻辑系统。核证逻辑的第一个标准的可能世界模型是姆克尔特切夫在1997年给出的姆克尔特切夫模型,菲廷在2005年正式给出了LP的可能世界模型,此外还有模式模型、极小模型等模型。核证逻辑的保守扩张问题也是一个重要问题。亚沃尔斯卡娅把可证明性逻辑GL和LP组合在一起得到了LPP,阿尔捷莫夫和诺吉娜给出了GLA的公理系统,二人也对同时带有经典模态算子和核证的系统S4LP和S4LPN进行了研究。阿尔捷莫夫引入了基于证据的知识,进而在知识的多主体逻辑的基础上得到了基于证据的知识系统,他给出了与TnLP, S4nLP和S5nLP对应的核证知识系统TnJ,S4nJ和S5nJ、,此外,还有对混合-JT、否定逻辑和核证摹状逻辑的研究。我们用T3J给出了泥孩难题的一种解决方法。菲廷给出了QLP,迪安和黑川用QLP分析了知道者悖论,但阿洛-科斯塔和岸田反对这种分析,量化的菲廷模型是在LP的菲廷模型的基础上添加了阶量化机制得到的,阿尔捷莫夫和亚沃尔斯卡娅提出了一阶证明逻辑FOLP,菲廷基于LP的菲廷模型给出了FOLP的可能世界模型,我们得到了一种新的系统QLP’,比QLP更为简单和自然。LP的表列系统是在2004年首次由雷恩给出,菲廷给出了S4LP的一种表列系统,雷恩之后给出了LP和S4LP的另一种表列系统,芬格尔给出了LP的两种分析的表列系统KELP和PREKELP,黑川给出了S4LPN的一种前缀表列系统TS4LPN,菲廷给出了K+J,S4LP,S4LPN和S5LPN的一种前缀表列系统。阿尔捷莫夫在1995年就给出了LP的实现概念和实现算法。勃列日涅夫和库兹涅茨给出了证明多项式至多是平方长度的实现算法,菲廷给出了直接对核证进行推理的机制,布吕纳、格奇和库兹涅茨证明了一种语法的实现定理,格奇和库兹涅茨之后给出了一种证明实现定理的更为一般的构造性的方法,并给出了统一实现定理,菲廷基于表列系统给出了LP的一种新的实现算法,还给出了LP的实现的一种Prolog执行程序。我们将菲廷的实现算法扩展到了FOLP的情况,并详细地证明了FOLP的准实现到实现的算法的正确性。核证逻辑源自主流认知理论、数理逻辑、计算机科学和人工智能等理论,它吸收了源自主流认知理论和证明论的基本原理,为直觉主义逻辑提供了一种算术语义,也为知识逻辑提供了一种新的以证据为基础的语义,它的出现解决了经典模态系统S4的哥德尔可证明性语义的问题和直觉主义命题逻辑的BHK语义的形式化问题,也解决了认知逻辑中“核证”这一概念在知识模型方面的问题,使认知逻辑的表达力更强了,核证项也为核证逻辑的复杂度问题提供了一种较为自然的衡量机制。当前,逻辑研究者对核证逻辑的研究仍然较为活跃,核证逻辑具有较多的改进余地、广阔的研究空间和巨大的发展潜力。更多还原

【Abstract】 The notion of justification is an important part in research of cognition since Plato. Plato has three criteria for knowledge:justification, truth and belief, however, though researchers of logic manage belief and truth in formal logic model of knowledge and belief, justification still lack management, justification is introduced into logic model of knowledge only after the emerge of justification logic.Godel speak about justification logic in1938, Artemov and Strassen give the prototype of the logic of proofs, Artemov gives LP, the logic of proofs, for the first time in1994, and gives the logic of proofs completely formally and relatively systematically in2001, from this we could get many new justification systems. The first normal possible world model for justification logic is Mkrtyclicv model, which is given by Mkrtychev in1997, Fitting gives the possible world model for LP normally in2005, there are other models such as modular model, minimal model, etc. The problem of conservative extension for justification logic is also an important question.Yavorskaya puts provability logic GL and LP together and gets LPP, Artemov and Nogina gives the axiomation of GLA, they also do research on system S4LP and S4LPN, which contain both classic modal operator and justification. Artemov introduces evidence-based knowledge, then gets evidence-based knowledge system based on multi-agent logic of knowledge, he gives justified knowledge system TnJ, S4nJ and S5nJ, which are the counterpart of TnLP, S4nLP and S5nLP, respectively. There are also research on hybrid-JT, denial logic, and justified descriptive logic. We give a resolution to the Muddy Children Puzzle through T3.Fitting gives QLP, Dean and Kurokawa analyze The Knower Paradox using QLP, but Arlo-Costa and Kishida object to this analyzation. Quantified Fitting model is got by adding first order quantification machinery based on Fitting model for LP, Artemov and Yavorskaya give first-order logic of proofs, Fitting gives possible world model for FOLP based on Fitting model for LP. We get a new system QLP, which is easier and more natural than QLP.The tableaux system for LP is first given by Renne in2004, Fitting gives a tableaux system for S4LP, Renne gives another tableaux system for LP and S4LP afterwards, Finger gives two analytic tableaux system KELP and preKELP for LP, Kurokawa gives a prefixed tableaux system TS4LPN for S4LPN, Fitting gives a prefixed tableaux system for K+J, S4LP, S4LPN, and S5LPN.Artemov gives the notion of realization and the algorithm of realization for LP in1995. Brezhnev and Kuznets give an algorithm of realization in which the proof polynomial is at most quadratic in length, Fitting gives a machinery in which we could reason with justification directly, Briinnler, Goetschi, and Kuznets prove a syntactic realization theorem, Goetschi and Kuznets then give a more general, constructive method of proving realization theorem, and give uniform realization theorem, Fitting gives a new algorithm of realization for LP based on tableaux system, and gives a Prolog implementation program of it. We extend Fitting’s algorithm of realization to the circumstance of FOLP, and prove the correctness of the algorithm of quasi-realization to realization of FOLP in detail.Justification logic stems from many theories such as mainstream epistemology, mathematical logic, computer science, artificial intelligence, etc. It absorbs basic principles of mainstream epistemology and proof theory, provides an arithmetical semantics to intuitionistic logic and a new semantics based on evidence to the logic of knowledge. The emerge of justification logic solves some problems:Godel’s provability semantics for classic modal system S4, formalization of BHK semantics for intuitionistic propositional logic, the notion of justification in epistemic logic in the model of knowledge. It makes the expressive power of epistemic logic more powerful, justification terms also provide natural measure machinery to the complexity of justification logic. Now, the research of justification logic is still very active, justification logic has much to improve, research, and develop.更多还原