Name
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. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.3233/FI-1994-2134 | Fundam. Inform. |
Keywords | Field | DocType |
theorem proving,semantic hyper-linking,model finding,basic procedure,instance-based theorem prover,input clause,ground instance,new ground instance,ground model,ground clause set,useful ground instance,ground set | Discrete mathematics,Automated theorem proving,Theoretical computer science,Model finding,Mathematical proof,Completeness (statistics),Mathematics,Semantics | Journal |
Volume | Issue | Citations |
21 | 3 | 6 |
PageRank | References | Authors |
0.53 | 10 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Heng Chu | 1 | 58 | 4.78 |
| David A. Plaisted | 2 | 1680 | 255.36 |