四川师范大学学报(自然科学版)2011,Vol.34Issue(5):635-639,5.DOI:10.3969/j.issn.1001-8395.2011.05.008
格值命题逻辑系统Ln ×2P(X)中广义文字的α-归结性
α-Resolution Fields of Generalized Literals in Lattice-valued Propositional Logic Ln×2P(X)
摘要
Abstract
Resolution based automatic reasoning is one of most important research directions in Al. Α-resolution method on lattice-valued logic based on lattice implication algebra provides alternative tool to handle the automatic reasoning problem with incomparability and fuzziness of information. It can refutably prove the α-unsatisfiability of clause set in lattice-valued logic system. We need to judge whether or not two generalized literals can form α-resolution pairs when we use a-resolution principle to refutably prove the a-unsatisfi-ability of a clausal set in Ln×2P(X). This paper discusses the resolvent of 1-IESF and other generalized literals and gets some determi-nations for a-resolution of two generalized literals.关键词
自动推理/归结域/格值逻辑/格蕴涵代数Key words
automatic reasoning/ resolution field/ lattice-valued logic/ lattice implication algebra分类
数理科学引用本文复制引用
张家锋,徐扬..格值命题逻辑系统Ln ×2P(X)中广义文字的α-归结性[J].四川师范大学学报(自然科学版),2011,34(5):635-639,5.基金项目
国家自然科学基金(60875034)和贵州省科技厅科学技术项目基金(2009GZ43286)资助项目 (60875034)