标记逻辑的TABLEAU判定过程  

TABLEAU CALCULUS FOR ANNOTATED LOGIC

作　　者：程晓春[1,2] 刘叙华[1,2] 

机构地区：[1]吉林大学计算机系 [2]吉林大学符号计算与知识工程开放实验室

出　　处：《软件学报》1996年第11期698-705,共8页Journal of Software

基　　金：国家自然科学基金;国家863高科技项目基金

摘　　要：标记逻辑是一种重要的次协调逻辑，和｜≈是标记逻辑中的２种推理关系．二者都是次协调的，可以用统一的方法处理一致的知识与不一致的知识，是单调的，有基于归结的证明论，但不能保持经典逻辑中合理的推理，如三段论．｜≈是非单调的，在前提一致时等价于经典逻辑的推理关系，但缺少有效的证明论．Annotated logic is one of the paraconsistent logics.The entailments in annotated logic are  and |≈. Both of them are paraconsistent, and can treat any set of formulae, either consistent or not, in a uniform way.  is monotonic, it has a resolution based sound and complete proof procedure, but some rational inferences of the classical logic, such as modus ponens, are no longer valid under it.|≈ is nonmonotonic. The classical inferences hold true under it when there is no contradiction. But no satisfactory proof theory for |≈ has been given. This paper will propose sound and complete decision Tableaux for  and |≈ respectively.

关 键 词：标记逻辑 TABLEAU方法 次协调逻辑 人工智能 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]