Theorem Proving by Covering Expressions
Abstract
This paper presents a reformulation of Gilmore's approach Rather than generate instances by saturation, the authors start with a few instances, convert to a nonredundant disjunctive normal form (DNF), and then use that DNF to help grade the choice of further instances The DNF in essence represents m a convenient form all the Boolean relations of the hteral instances Viewed differently, the DNF provides a concise description of clauses which, ffadded, would produce unsatlsfiablhty Thus the mare activity in the theorem-proving process Js analyzing possible new instances of input clauses and their relationship to the already present instances Some examples from an interactive program are given
Cite
Text
Henschen and Evangelist. "Theorem Proving by Covering Expressions." International Joint Conference on Artificial Intelligence, 1977. doi:10.1145/322139.322140Markdown
[Henschen and Evangelist. "Theorem Proving by Covering Expressions." International Joint Conference on Artificial Intelligence, 1977.](https://mlanthology.org/ijcai/1977/henschen1977ijcai-theorem/) doi:10.1145/322139.322140BibTeX
@inproceedings{henschen1977ijcai-theorem,
title = {{Theorem Proving by Covering Expressions}},
author = {Henschen, Lawrence J. and Evangelist, W. M.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1977},
pages = {541-542},
doi = {10.1145/322139.322140},
url = {https://mlanthology.org/ijcai/1977/henschen1977ijcai-theorem/}
}