---
title: "A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems"
authors:
  - "Antoni Ligeza"
doi: ""
url: "https://ijcai.org/proceedings/1993/19"
pdf: "https://ijcai.org/proceedings/1993/0019.pdf"
venue: "Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence"
year: 1993
pages: "132-136"
track: "Automated Reasoning"
keywords:
---

# A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems

Antoni Ligeza

*Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence*, pages 132-136.

## Abstract

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-resolution, 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.