Consolution and its Relation with Resolution
Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 132-135.
Abstract
In this paper the method of consolution for clause form theorem proving is introduced . Consolution is based on the connection method. This means that in a consolution derivation the paths through the input formula are checked for complementarity. In contrast to resolution this checking can be done in a systematic way as in any connection calculus. It is proved that the consolution calculus presented here is sound and complete and that it can simulate resolution step by step and is a generalization of resolution. It combines the advantages of the connection method such as the directedness of search with the advantages of resolution such as the possibility of the use of lemmata.
@inproceedings{ijcai1991p20,
title = {Consolution and its Relation with Resolution},
author = {Eder, Elmar},
booktitle = {Proceedings of the Twelfth International Joint Conference on
Artificial Intelligence, {IJCAI-91}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {John Mylopoulos and Ray Reiter},
pages = {132--135},
year = {1991},
month = {8},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1991/20},
}
TY - CPAPER TI - Consolution and its Relation with Resolution AU - Eder, Elmar T2 - Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91 PB - International Joint Conferences on Artificial Intelligence PY - 1991 SP - 132 EP - 135 UR - https://ijcai.org/proceedings/1991/20 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
