---
title: "Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers"
authors:
  - "Dennis de Champeaux"
doi: ""
url: "https://ijcai.org/proceedings/1979/45"
pdf: "https://ijcai.org/proceedings/1979/0045.pdf"
venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence"
year: 1979
pages: ""
track: ""
keywords:
---

# Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers

Dennis de Champeaux

*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