一种改进的OL归结——SOL归结

计算机工程与科学

一种改进的OL归结——SOL归结

刘清华，徐扬

（西南交通大学信息科学与技术学院，四川成都 610031）

收稿日期:2017-12-25 修回日期:2018-03-22 出版日期:2019-01-25 发布日期:2019-01-25
基金资助:
国家自然科学基金（61673320）；中央高校基本科研业务费专项资金（2682018ZT10）

An improved OL resolution: SOL resolution

LIU Qinghua，XU Yang

（School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610031,China）

Received:2017-12-25 Revised:2018-03-22 Online:2019-01-25 Published:2019-01-25

摘要/Abstract

摘要：

1973年,Chang和Lee将线性归结与有序归结相结合，提出了有序线性归结，即OL归结,极大地提高了线性归结的效率和机械性。然而，OL归结并不是一种完备的归结方法。在OL归结的约化条件的基础上提出了强约化的概念。强约化条件对中心有信息有序子句的约化做了进一步的限制，且该强约化条件是约化条件的一种特例。在强约化条件的基础上，还提出了一种改进的OL归结——SOL归结，并证明了其完备性。

关键词: OL归结, SOL归结, 强约化, 完备性

Abstract:

In 1973, Chang and Lee combined linear resolution with ordered resolution and proposed an ordered linear resolution, namely OL resolution. It greatly improves the efficiency and mechanicality of linearization. However, the OL resolution is not a complete resolution method. We propose a concept of strong reduction based on the reduction condition of the OL resolution. Strong reduction further restricts the reduction condition of ordered informational center clauses, and the strong reduction is a special case of the reduction condition. Based on strong reduction, we also put forward an improved OL resolution, called SOL resolution, and prove its completeness.

Key words: OL resolution, SOL resolution, strong reduction, completeness

刘清华，徐扬. 一种改进的OL归结——SOL归结[J]. 计算机工程与科学.

LIU Qinghua，XU Yang. An improved OL resolution: SOL resolution[J]. Computer Engineering & Science.

[1]	吴佳伟，刘国华，王梅. 匿名隐私保护模型中不确定性数据的建模问题研究[J]. J4, 2011, 33(9): 7-12.
[2]	王俐莉王元元张兴元. 命题演算形式系统在Isabelle／HOL中的形式化[J]. J4, 2008, 30(10): 67-68.