Analytic resolution in theorem proving |
| |
Authors: | D Brand |
| |
Affiliation: | Department of Computer Science, University of Toronto, Toronto, Ontario, Canada |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|