Ordering-Based Strategies for Horn Clauses
Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 118-124.
Abstract
Two new theorem-proving procedures for equational Horn clauses are presented. The largest literal is selected for paramodulation in both strategies, except that one method treats positive literals as larger than negative ones and results in a unit strategy. Both use term orderings to restrict paramodulation to potentially maximal sides of equations and to increase the amount of allowable simplification (demodulation). Completeness is shown using proof orderings.
Nachum Dershowitz. 1991. Ordering-Based Strategies for Horn Clauses. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91. IJCAI, 118–124. https://ijcai.org/proceedings/1991/18
Dershowitz, N. (1991). Ordering-Based Strategies for Horn Clauses. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91 (pp. 118–124). IJCAI. https://ijcai.org/proceedings/1991/18
@inproceedings{ijcai1991p18,
title = {Ordering-Based Strategies for Horn Clauses},
author = {Dershowitz, Nachum},
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 = {118--124},
year = {1991},
month = {8},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1991/18},
}
TY - CPAPER TI - Ordering-Based Strategies for Horn Clauses AU - Dershowitz, Nachum T2 - Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91 PB - International Joint Conferences on Artificial Intelligence PY - 1991 SP - 118 EP - 124 UR - https://ijcai.org/proceedings/1991/18 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
