核证的概念自柏拉图时代以来就是认知研究中的一个重要部分,柏拉图对知识有三个准则：核证,真,信念,但是,尽管逻辑研究者在知识和信念的形式化的逻辑模型中处理了信念和真,核证却一直缺少相应的处理,直到核证逻辑出现后,核证才被引入到知识的逻辑模型中。哥德尔在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语义的形式化问题,也解决了认知逻辑中“核证”这一概念在知识模型方面的问题,使认知逻辑的表达力更强了,核证项也为核证逻辑的复杂度问题提供了一种较为自然的衡量机制。当前,逻辑研究者对核证逻辑的研究仍然较为活跃,核证逻辑具有较多的改进余地、广阔的研究空间和巨大的发展潜力。