MODEL FINDING IN SEMANTICALLY GUIDED INSTANCE-BASED THEOREM PROVING
Heng Chu, David A. Plaisted · Fundamenta Informaticae · 1994
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 unsatisfiab