计算机科学与探索Issue(2)：221-226,6.DOI:10.3778/j.issn.1673-9418.1409022
基于布尔语义的Gentzen推导模型
Gentzen Deduction Model Based on Boolean Logic Semantics
摘要
Abstract
Deduction systems are important arts of searching technology. This paper gives a new correspondence between the propositional logic and Boolean algebra, where an inequation is corresponding to a Gentzen sequent, so that the inequation is true in every Boolean algebra if and only if the Gentzen sequent is provable. In information retrieval, the information inference can effectively turn into the operation on poset. Precisely, the logical language for the propositional logic contains operators Ø'Ù'Ú;the terms instead of formulas are defined (a|Øt|t1 Ù t2|t1 Ú t2 , where a is an element) and used to represent elements in Boolean algebra. This paper defines an assignment v using Boolean algebra as its domain, and assigns the terms to be the element in Boolean algebra. The sequence ΓÞΔ is satisfied if tv £tv. Finally, this paper gives a Gentzen system to prove the soundness and completeness theorem.关键词
布尔代数/命题逻辑/不等式/完备性Key words
Boolean algebra/proposition logic/inequation/completeness分类
信息技术与安全科学引用本文复制引用
陈博,眭跃飞..基于布尔语义的Gentzen推导模型[J].计算机科学与探索,2015,(2):221-226,6.基金项目
The National Natural Science Foundation of China under Grant Nos.91224006,61173063,61035004,61203284,309737163(国家自然科学基金) （国家自然科学基金）
