Name
Abstract | ||
|---|---|---|
CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. In this article, we describe the system architecture and major inference rules used in CLIN-S. |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1023/A:1005875128672 | J. Autom. Reasoning |
Keywords | Field | DocType |
automated theorem proving,competition,CLIN-S,semantics,hyper-linking,resolution | Computer-assisted proof,Discrete mathematics,Inference,Automated theorem proving,Algorithm,Mathematical proof,Proof complexity,Rule of inference,Mathematics,Formal proof,Proof assistant | Journal |
Volume | Issue | ISSN |
18 | 2 | 1573-0670 |
Citations | PageRank | References |
7 | 0.43 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Heng Chu | 1 | 58 | 4.78 |
| David A. Plaisted | 2 | 1680 | 255.36 |