Deletion-Directed Search in Resolution-Based Proof Procedures
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 set of retained clauses. E-representation, a new clause deletion rule which is fundamental to the operation of the search strategy, is also described.
Cite
Text
Gelperin. "Deletion-Directed Search in Resolution-Based Proof Procedures." International Joint Conference on Artificial Intelligence, 1973.Markdown
[Gelperin. "Deletion-Directed Search in Resolution-Based Proof Procedures." International Joint Conference on Artificial Intelligence, 1973.](https://mlanthology.org/ijcai/1973/gelperin1973ijcai-deletion/)BibTeX
@inproceedings{gelperin1973ijcai-deletion,
title = {{Deletion-Directed Search in Resolution-Based Proof Procedures}},
author = {Gelperin, David},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1973},
pages = {47-50},
url = {https://mlanthology.org/ijcai/1973/gelperin1973ijcai-deletion/}
}