A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems
Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. 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.
@inproceedings{ijcai1993p19,
title = {A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems},
author = {Ligeza, Antoni},
booktitle = {Proceedings of the Thirteenth International Joint Conference on
Artificial Intelligence, {IJCAI-93}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Ruzena Bajcsy},
pages = {132--136},
year = {1993},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1993/19},
}
TY - CPAPER TI - A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems AU - Ligeza, Antoni T2 - Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, IJCAI-93 PB - International Joint Conferences on Artificial Intelligence PY - 1993 SP - 132 EP - 136 UR - https://ijcai.org/proceedings/1993/19 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
