Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers
Proceedings of the Sixth International Joint Conference on Artificial Intelligence. .
Abstract
Two pre-processors for theorem provers are described, which when applicable, will lead to search space simplification. Both were implemented and integrated with an existing resolution type connection graph theorem prover. Examples are provided which confirm our claim of search space simplification. Key words and phrases: Theorem proving, pre-processing, search space simplification
Dennis de Champeaux. 1979. Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers. In Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79. IJCAI, https://ijcai.org/proceedings/1979/45
de Champeaux, D. (1979). Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers. In Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79. IJCAI. https://ijcai.org/proceedings/1979/45
@inproceedings{ijcai1979p45,
title = {Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers},
author = {de Champeaux, Dennis},
booktitle = {Proceedings of the Sixth International Joint Conference on
Artificial Intelligence, {IJCAI-79}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Bruce G. Buchanan},
year = {1979},
month = {8},
url = {https://ijcai.org/proceedings/1979/45},
}
TY - CPAPER TI - Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers AU - de Champeaux, Dennis T2 - Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79 PB - International Joint Conferences on Artificial Intelligence PY - 1979 UR - https://ijcai.org/proceedings/1979/45 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
