Computer Science

Colloquium Details

Theorem proving strategies: a search-oriented taxonomy

Abstract

This talk presents a taxonomy of strategies for fully-automated general-purpose first-order theorem proving. It includes both forward-reasoning ordering-based strategies, such as those based on resolution, and backward-reasoning subgoal-reduction strategies, such as those based on tableaux, which do not appear together often.

Unlike traditional presentations that emphasize logical inferences, this presentation gives equal weight to the inference and search components of theorem proving, which are equally important in practice. For this purpose, it is necessary to define properly several notions about search in theorem proving, which are usually thought of only intuitively, or remain hidden in implementations. These include the search plan, the search space for different types of strategies, which part of the search space is active, what is the proof that eventually the strategy may extract from the generated search space. The resulting model of search in theorem proving has been also applied by the author as a basis for both design and analysis of strategies.