信念修正开放过程模式可判定公式表达能力  

Expressive power of decidable subclasses of open proxcheme

作　　者：张伟 柳玉辉[2] 

机构地区：[1]东北大学计算机科学与工程学院,沈阳110819 [2]东北大学研究院,沈阳110819

出　　处：《吉林大学学报（工学版）》2016年第6期2021-2026,共6页Journal of Jilin University:Engineering and Technology Edition

基　　金：国家科技支撑计划项目(2014BAI17B01);软件开发环境国家重点实验室开放课题项目(SKLSDE-2012KF-02)

摘　　要：提出了一种可以在两个极大可判定前缀词公式类上实现信念修正OPEN过程模式的算法,该算法从初始形式理论出发,依据不断获取的新事实信息,迭代修正形式理论,完成形式理论的进化。探讨了OPEN过程模式的两种可判定公式类的表达能力,证明了其表达能力强于一阶逻辑的子集FO^2和模态逻辑,并给出了实际应用例子。An algorithm for OPEN proxcheme is proposed that functions in the two maximal decidable classes of first-order logic. The algorithm iteratively revises the formal theories according to new information and completes the evolution of the formal theories. The expressive power of the OPEN proxcheme is discussed. It is demonstrated that the OPEN proxcheme and R-calculus preserve the decidability of formulas in the two maximal decidable classes. Since the decision problem for modal logic and FO2 can be transferred to that of the two maximal decidable classes, it can be concluded that the OPEN proxcheme and R-calculus are more expressive than the modal logic and FO2. Practical examples, such as hardware description and verification, are provided.

关 键 词：人工智能 信念修正 开放过程模式 可判定公式类 表达能力 定理机器证明 

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