Name
Abstract | ||
|---|---|---|
We develop two applications of middle-out reasoning in inductive proofs: Logic programsynthesis and the selection of induction schemes. Middle-out reasoning as part of proof planningwas first suggested by Bundy et al [Bundy et al 90a]. Middle-out reasoning uses variablesto represent unknown terms and formulae. Unification instantiates the variables in the subsequentplanning, while proof planning provides the necessary search control.Middle-out reasoning is used for synthesis by... |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1007/BF00244461 | J. Autom. Reasoning |
Keywords | Field | DocType |
Automated theorem proving,proof planning,induction,logic program synthesis,metavariables,higher-order unification | Automated reasoning,Discrete mathematics,Unification,Automated theorem proving,Automated proof checking,Algorithm,Mathematical proof,Deductive reasoning,Reasoning system,Proof planning,Mathematics | Journal |
Volume | Issue | ISSN |
16 | 1-2 | 0168-7433 |
Citations | PageRank | References |
20 | 6.57 | 25 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ina Kraan | 1 | 183 | 18.79 |
| David A. Basin | 2 | 4930 | 281.93 |
| A. Bundy | 3 | 3713 | 532.03 |