Heng Chu, David A. Plaisted
Semantic hyper-linking [Plaisted et al., 1992, Chu and Plaisted, 1993, Chu and Plaisted, 1992] has been proposed recently to use semantics with hyper-linking [Lee and Plaisted, 1992], an instance-based theorem proving technique. Ground instances are generated until an unsatisfiable ground set is obtained; semantics is used to greatly reduce the search space. One disadvantage of semantic hyper-linking is,that large ground literals, if needed in the proofs, sometimes are hard to generate. In this paper we propose rough resolution, a refinement of resolution [Robinson, 1965], to only resolve upon maximum literals, that are potentially large in ground instances, and obtain rough resoluents. Rough resolvents can be used by semantic hyper-linking to avoid generating large ground literals since maximum literals have been deleted. As an example, we will show how rough resolution helps to prove LIM3 [Bledsoe, 1990 , which cannot be proved using semantic 9 hyper-linking only. We will also show other results in which rough resolution helps to find the proofs faster. Though incomplete, rough resolution can be used with other complete methods that prefer small clauses.