Sub-Problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers
Abstract
Abstract. Properties are proved about INSTANCE, a theorem prover module that recognizes that a formula is a special case and/or an alphabetic variant of another formula, and about INSURER, another theorem prover module that decomposes a problem, represented by a formula, into independent subproblems, using a conjunction. The main result of INSTANCE is soundness; the main result of INSURER is a maximum decomposition into subproblems (with some provisos). Experimental results show that a connection graph theorem prover extended with these modules is more effective than the resolution-based connection graph theorem prover alone.
Cite
Text
de Champeaux. "Sub-Problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers." International Joint Conference on Artificial Intelligence, 1979.Markdown
[de Champeaux. "Sub-Problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers." International Joint Conference on Artificial Intelligence, 1979.](https://mlanthology.org/ijcai/1979/dechampeaux1979ijcai-sub/)BibTeX
@inproceedings{dechampeaux1979ijcai-sub,
title = {{Sub-Problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers}},
author = {de Champeaux, Dennis},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1979},
pages = {191-196},
url = {https://mlanthology.org/ijcai/1979/dechampeaux1979ijcai-sub/}
}