Ina Kraan, David Basin, Alan Bundy  @ NUS Home/Search
Context Related
| informatik.unifreiburg.d...iclp10.ps.Z dream.dai.ed.ac.uk/publi...pub638.ps.gz Cached: PS.gz PS PDF Image Update Help From: informatik.unifreiburg.de...pubs (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: Logic programs can be synthesized as a by-product of the planning of their verification proofs. This is achieved by using higher-order variables at the proof planning level, which become instantiated in the course of planning. We illustrate two uses of such variables in proof planning for program synthesis, one for synthesis proper and one for the selection of induction schemes. We demonstrate that the use of these variables can be restricted naturally in such a way that terms containing them... (Update)
Context of citations to this paper: More
.... of meta level inference systems in this way is not new in the field of automated theorem proving (see for example [Bundy et al. 90a, Kraan et al. 93b] it is novel in the field of process verification. ffl We have also used meta level information to guide the instantiation of...
.... ed variable until a witness term is found during the planning process (such a postponement is also called a middle out reasoning process [14]) After splitting P [MV ] Q[MV ] into the two subgoals P [MV ] and Q[MV ] the planner focuses on P [MV ] rst. A meta reasoning process...
Cited by: More
Certifying Solutions to - Permutation Group Problems (2003) (Correct)
A Unified View of Program Schemas and Proof Methods - Flener, Richardson (Correct)
Using Proof in Transformation Synthesis for Automatic.. - Cook (2001) (Correct)
Similar documents (at the sentence level):
14.2%: Logic Program Synthesis via Proof Planning - Kraan, Basin, Bundy (1993) (Correct)
Active bibliography (related documents): More All
0.6: Middle-Out Reasoning for Synthesis and Induction - Kraan, Basin, Bundy (1995) (Correct)
0.3: Guiding Synthesis Proofs - Lombart, Wiggins, Deville (1993) (Correct)
0.2: Logic Program Synthesis - Deville, Lau (1993) (Correct)
Similar documents based on text: More All
0.7: Proof Planning and Program Synthesis: a Survey - Richardson (2002) (Correct)
0.3: Mollusc: A General Proof-Development Shell for.. - Richards, Kraan.. (1994) (Correct)
0.3: Rippling on Relational Structures - Vincent Lombart Yves (1994) (Correct)
Related documents from co-citation: More All
10: KIDS: A Semi-automatic Program Development System - Smith - 1990
9: The use of explicit plans to guide inductive proofs - Bundy - 1988
9: Logic program synthesis via proof planning - Kraan, Basin et al. - 1993
BibTeX entry: (Update)
Kraan, I., Basin, D., Bundy, A. (1993). Middle-out reasoning for logic program synthesis. In 10th International Conference on Logic Programming (ICLP93), pages 441--455, Budapest Hungary. http://citeseer.comp.nus.edu.sg/123713.html More
@misc{ kraan93middleout,
author = "I. Kraan and D. Basin and A. Bundy",
title = "Middle-out reasoning for logic program synthesis",
text = "Kraan, I., Basin, D., Bundy, A. (1993). Middle-out reasoning for logic
program synthesis. In 10th International Conference on Logic Programming
(ICLP93), pages 441--455, Budapest Hungary.",
year = "1993",
url = "citeseer.comp.nus.edu.sg/123713.html" }
Citations (may not include all citations):1838 Foundations of Logic Programming (context) - Lloyd - 1987
392 A Computational Logic (context) - Boyer, Moore - 1979
251 A logic programming language with lambda abstraction - Miller - 1990
233 The formulae-as-types notion of construction (context) - Howard - 1980
226 The use of explicit plans to guide inductive proofs - Bundy - 1988
168 Rippling: A heuristic for guiding inductive proofs - Bundy, Stevens et al. - 1991
126 Higher-order critical pairs (context) - Nipkow - 1991
87 The Oyster-Clam system (context) - Bundy, van Harmelen et al. - 1990
50 Derivation of logic programs (context) - Hogger - 1981
30 The synthesis of logic programs from inductive proofs (context) - Bundy, Smaill et al. - 1990
28 Logic program synthesis via proof planning - Kraan, Basin et al. - 1993
24 A rational reconstruction and extension of recursion analysi.. - Bundy, van Harmelen et al. - 1989
23 Extracting logic programs from proofs that use extended Prol.. (context) - Fribourg - 1990
21 Turning eureka steps into calculations in automatic program .. (context) - Bundy, Smaill et al. - 1990
20 Synthesis of induction orderings for existence proofs - Hutter - 1992
17 Synthesis and transformation of logic programs in the Whelk .. (context) - Wiggins - 1992
6 A unification algorithm for lambda calculus (context) - Huet - 1975
6 Unification of higher-order patterns in linear time and spac.. (context) - Qian - 1992
5 International Series in Logic Programming (context) - Deville, Systematic - 1990
4 Synthesis and transformation of logic programs through const.. (context) - Wiggins, Bundy et al. - 1991
The graph only includes citing articles where the year of publication is known.
Documents on the same site (http://www.informatik.uni-freiburg.de/~basin/pubs/pubs.html): More
A Modular Presentation of Modal Logics in a Logical.. - Basin, Matthews.. (Correct)
A Recursion Planning Analysis of Inductive Completion - Barnett, Basin, Hesketh (1994) (Correct)
Program Development Schemata as Derived Rules - Anderson, Basin (1998) (Correct)
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.