A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems
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-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
Cite
Text
Ligeza. "A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems." International Joint Conference on Artificial Intelligence, 1993.Markdown
[Ligeza. "A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems." International Joint Conference on Artificial Intelligence, 1993.](https://mlanthology.org/ijcai/1993/ligeza1993ijcai-note/)BibTeX
@inproceedings{ligeza1993ijcai-note,
title = {{A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems}},
author = {Ligeza, Antoni},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1993},
pages = {132-137},
url = {https://mlanthology.org/ijcai/1993/ligeza1993ijcai-note/}
}