Name
Abstract | ||
|---|---|---|
We propose a novel approach to automating the synthesis of logic programs: Logicprograms are synthesized as a by-product of the planning of a verification proof. Theapproach is a two-level one: At the object level, we prove program verification conjecturesin a sorted, first-order theory. The conjectures are of the form 8args\Gamma\Gamma\Gamma\Gamma!: prog(args\Gamma\Gamma\Gamma\Gamma!) $spec(args\Gamma\Gamma\Gamma\Gamma!). At the meta-level, we plan the object-level... |
Year | Venue | Keywords |
|---|---|---|
1993 | ICLP | logic program synthesis,middle-out reasoning,automated theorem proving,first order |
Field | DocType | ISSN |
Computational logic,Automated reasoning,Separation logic,Programming language,Program synthesis,Computer science,Algorithm,Proof theory,Bunched logic,Theoretical computer science,Mathematical proof,First-order logic | Conference | 1061-0464 |
ISBN | Citations | PageRank |
0-262-73105-3 | 17 | 1.15 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ina Kraan | 1 | 183 | 18.79 |
| David Basin | 2 | 17 | 1.15 |
| A. Bundy | 3 | 3713 | 532.03 |