Analytic resolution in theorem proving

摘要

Analytic resolution is a proof procedure for predicate calculus based on the ideas of semantic trees and analytic tableaux. It is related to the unit preference with set-of-support strategy, and incorporates some features of model elimination. The philosophy is to expect and compensate for “blind alleys” by a stack discipline. This eliminates pollution of the search space by a bad choice of the next step in a proof. Experimental results included compare favourably with others from the literature.