A Model Elimination Calculus for Generalized Clauses
Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 126-130.
Abstract
Generalized clauses differ from (ordinary) clauses by allowing conjunctions of literals in the role of (ordinary) literals , i.e. they are disjlmctions of conjunctions of simple literals. An advantage of this clausal form is that implications with conjunctive conclusions or disjunctive premises are not split into multiple clallSes. An extension of Loveland's model elimination calculus [Loveland, 1969a, Loveland, 1978] is presented able to deal with such generalized clauses. Furthermore we describe a method for generating lemmas that. correspond to valid instances of cmljunctive conclusions. Using these lemmas it is po11sible to avoid multiple proofs of the premises of implications with conjunctive conclusions.
@inproceedings{ijcai1991p19,
title = {A Model Elimination Calculus for Generalized Clauses},
author = {Bollinger, Toni},
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 = {126--130},
year = {1991},
month = {8},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1991/19},
}
TY - CPAPER TI - A Model Elimination Calculus for Generalized Clauses AU - Bollinger, Toni T2 - Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91 PB - International Joint Conferences on Artificial Intelligence PY - 1991 SP - 126 EP - 130 UR - https://ijcai.org/proceedings/1991/19 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
