• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

Computer Engineering & Science

Previous Articles     Next Articles

An improved OL resolution: SOL resolution

LIU Qinghua,XU Yang   

  1. (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:

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