Name
Abstract | ||
|---|---|---|
We have developed a theorem prover for the full first order logic, by compiling clauses into proof procedures. These procedures exploit a set of abstract machine primitives for full unification and primitives which provide completeness and soundness for the proof procedure. These primitives are part of a Common Runtime Support which enables mixing code from various high level languages. Our theorem prover can thus be used as a component in a larger application, which may be written in any mixture of C, Lisp and Prolog. We show first how to compile Horn clauses along the lines of Prolog. A full first-order logic theorem prover is then produced by compiling predicates into code which uses full unification, a complete search strategy and a complete inference procedure. |
Year | DOI | Venue |
|---|---|---|
1991 | 10.1007/3-540-54712-6_258 | AI*IA |
Keywords | Field | DocType |
effiecient compilation,first order predicates,first order | Programming language,Horn clause,Computer science,Unification,Lisp,Automated theorem proving,First-order logic,Prolog,Soundness,Proof procedure | Conference |
ISBN | Citations | PageRank |
3-540-54712-6 | 0 | 0.34 |
References | Authors | |
2 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Giuseppe Attardi | 1 | 545 | 101.27 |
| Mauro Gaspari | 2 | 286 | 37.38 |
| Pietro Iglio | 3 | 139 | 16.58 |