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

Expressive power of decidable subclasses of open proxcheme

提出了一种可以在两个极大可判定前缀词公式类上实现信念修正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.