A note on backward dual resolution and its application to proving completeness of rule-based systems
Antoni Ligęza · 1993
In this paper, a method of theorem proving dual to resolution method is presented in brief. The investigated method is called backward dual resolution or bd-re solution, for short. The main idea of bd-resolution consists in proving validity of a formula in disjunctive normal form, by generating an empty tautology formula from it; it is shown that the initial formula is a logical consequence of the obtained tautology. An idea of the theorem proving method is outlined, and its application to checking completeness of rulebased systems is investigated. A formal definition of completeness and specific completeness are stated and an algorithm for completeness verification is proposed. Moreover, a generalized bd-resolution aimed at proving completeness under intended interpretation is defined. 1