当代中国逻辑学研究
二 非经典逻辑的自动推理
|
来 源
：
|
当代中国逻辑学研究2009 \ - |
作 者
：
|
- |
浏览次数
：
|
13 | ||
|
摘 要
：
|
利用计算机进行自动推理一直是热门的研究领域。卡内基梅隆大学认知心理学家Alen Newell因创立了Logic Machine Theory和General Problem Solver（与Herb Simon一起）而获得1975年图灵奖。Lo Libo, “On the computational complexity of the theory of abelian groups”， Ann.Pure Appl.Logic， Vol.37， No.3。M.S.Ying, “A logic for approximate reasoning”， J.Symbolic Logic， Vol.59， No.3， M.Hennessy, H.Lin， “Proof Systems for Message-Passing Process Algebras”， Formal Aspects of Computing， Vol.8。 | ||||||
|
关键词
：
|
Vol Logic 学报 Comput Sci 数学 Theory 定理 Symbolic Problem 计算机 |
||||||
在线阅读
二 非经典逻辑的自动推理
字体：大中小
刘叙华与他人合作提出了算子模糊逻辑（fuzzy operator logic），并建立了这种逻辑的推演系统。这个推演系统实际上就是基于消解原理的一种推广。他们证明了系统的可靠性与完全性sup[341]。评论者认为这是不确定自动推理领域的重要工作。刘叙华和司徒芊提出算子模糊逻辑中的广义λ-消解方法，证明了它和广义λ-归结的联合使用，对于λ-不可满足广义子句集是完备的sup[60]。唐日昆和刘叙华在广义λ-归结方法中引进删除策略，并证明：以λ-蕴涵为基础的删除策略不破坏广义λ-归结方法的完备性sup[106]。邓安生和刘叙华在布尔算子Fuzzy逻辑中引入公式的恒假水平的概念，证明了归结原理在定性和定量这两种度量意义下的广义完备性sup[16]。
吴尽昭由给定的有穷值逻辑系统中的一组公式T及一个公式A出发，构造出了一组有理数域上的多项式PS，使得A是T的逻辑结论，当且仅当PS定义的代数簇为空集，当且仅当PS生成的理想是平凡理想。从而，利用特征列方法和Groebner基方法，给出了判定多值逻辑推理的两种算法sup[141]。
孙吉贵和刘叙华提出了一种模态归结的弱包含删除策略，证明了使用弱包含删除策略模态归结的完备性。从而将Auffray等人提出的开问题——模态归结包含删除策略的完备性向前推进了一步sup[103]。他们提出了一种基于标准子句集的模态归结方法的变型，称之为标准模态归结。证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发，使用标准模态归结推出空子句的演绎。从而证明了对于不可满足标准子句集、标准模态归结是完备的sup[177]。他们将经典逻辑的Davis-Putnam纯文字化简规则推广到了命题模态逻辑D系统的自动演绎中，并给出了一些刻画D逻辑自动演绎特征的化简规则。这些化简规则通过对公式、子公式和公式集的有效性（或不可满足性）的有条件的判断，进行证明过程的剪枝和化简，以提高D逻辑自动演绎的效率，这些化简规则可用于D逻辑的任意一种推理实现系统，在机器上是容易实现的sup[15]。
张健研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理证明器进行推理。文中指出，该方法在理论上保持了正规命题模态逻辑的可判定性。还给出了一些试验结果，说明该方法是实际可行的sup[158]。
沈榆平、赵希顺则研究了回答集语义下的逻辑程序的自动推理技术。他们提出并实现了破圈启发方法与基部限制式前向搜索技术。与其他逻辑程序系统比较，沈和赵的系统能高效地解决相变难区域中推理问题sup[376]。
徐扬和王伟对格值命题逻辑系统LP（X）中基于α-归结原理的α-自动推理方法进行了研究，给出了用符号矩阵表示一类简单的广义子句集合（只含命题变元和非正则1-IESF广义文字）的方法，把α-归结原理转换成矩阵的列变换sup[351]。徐扬、秦克云等基于格蕴涵代数的格值命题逻辑系统LP4（X）的相关概念和结果，给出了LP4（X）上的归结原理，并证明了其可靠性和完备性。四值命题逻辑系统LP4（X）作为含有不可比真值的一种基本且重要的格蕴涵代数结构，其上归结原理的研究为归结算法的实现提供了理论基础，从而为处理含有不可比真值的格值逻辑系统在智能推理系统中的实际应用提供了有力的支持sup[72]。
王国俊、惠晓静等研究了模糊逻辑的分离规则（FMP），给出了解决FMP的新算法sup[344]。
显示更多