Deletion-Directed Search in Resolution-Based Proof Procedures
Proceedings of the Third International Joint Conference on Artificial Intelligence. Theorem Proving and Logic: 1. Pages 47-49.
Abstract
The operation of a deletion-directed search strategy for resolution-based proof procedures is discussed. The strategy attempts to determine the satisfiability of a set of input clauses while at the same time minimizing the cardinality of the s·et of retained clauses. E-representation, a new clause deletion rule which is fundamental to the operation of the search strategy, is also described.
David Gelperin. 1973. Deletion-Directed Search in Resolution-Based Proof Procedures. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73. IJCAI, 47–49. https://ijcai.org/proceedings/1973/7
Gelperin, D. (1973). Deletion-Directed Search in Resolution-Based Proof Procedures. In Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73 (pp. 47–49). IJCAI. https://ijcai.org/proceedings/1973/7
@inproceedings{ijcai1973p7,
title = {Deletion-Directed Search in Resolution-Based Proof Procedures},
author = {Gelperin, David},
booktitle = {Proceedings of the Third International Joint Conference on
Artificial Intelligence, {IJCAI-73}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Nils J. Nilsson},
pages = {47--49},
year = {1973},
month = {8},
note = {Theorem Proving and Logic: 1},
url = {https://ijcai.org/proceedings/1973/7},
}
TY - CPAPER TI - Deletion-Directed Search in Resolution-Based Proof Procedures AU - Gelperin, David T2 - Proceedings of the Third International Joint Conference on Artificial Intelligence, IJCAI-73 PB - International Joint Conferences on Artificial Intelligence PY - 1973 SP - 47 EP - 49 UR - https://ijcai.org/proceedings/1973/7 ER -Copied
Machine-readable versions of this paper, for tools and AI agents: