MODEL FINDING IN SEMANTICALLY GUIDED INSTANCE-BASED THEOREM PROVING

Article type: Research Article

Authors: Chu, Heng | Plaisted, David A.

Affiliations: Department of Computer Science, University of North Carolina, Chapel Hill, NC 27599-3175, USA, {chu|plaisted}@cs.unc.edu

Abstract: Semantic hyper-linking has recently been proposed as a way to use semantics in an instance-based theorem prover. The basic procedure is to use semantics to help generate ground instances of the input clauses until the ground clause set is unsatisfiable. If the ground set is satisfiable, models are constructed periodically to guide generation of new ground instances and change the models, until no model can be constructed and a proof is found. In this paper we discuss some model finding strategies that can generate useful ground instances, without using semantics, to change the ground models. We show that such strategies are helpful and will not increase the search space of semantic hyper-linking. They also retain the completeness of semantic hyper-linking. In addition, since using semantics is often expensive and semantics is not used in those model finding strategies, they help to find proofs earlier and faster.

DOI: 10.3233/FI-1994-2134

Journal: Fundamenta Informaticae, vol. 21, no. 3, pp. 221-235, 1994