Bundy, A., Smaill, A. and Wiggins, G.: The Synthesis of Logic Programs from Inductive Proofs. In J. W. Lloyd (ed.) Proceedings of Esprit Symposium on Computational Logic, pp. 135-149. Springer-Verlag, 1990.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....(not included in the paper) consist of about two pages of program code. Thus, it would be tractable to formally prove the prototype compiler implements the specification for a given set of inputs, assuming a suitable semantics of (a subset of) Prolog [Llo87] if this is of concern (e.g. see [BSW90]) In addition, optimization using transformation of logic programs [ClL92]would be possible. However this has not (yet) been attempted by the authors, since the prototype has simply been used as a means of quickly animating the specification mechanically. Proofs of termination and non violation ....

Bundy, A., Smaill, A. and Wiggins G.: The Synthesis of Logic Programs from Inductive Proofs. In Lloyd, J. W. (ed.) Computational Logic. Springer-Verlag, Basic research series, pp. 135--149, 1990.

....rules. In this regard, the speci c contribution of our chapter consists in providing a method for program synthesis which ensures the correctness w.r.t. the perfect model semantics. Also related to our rules and strategies approach, is the proofs as programs approach (see, for instance, [8,25] for its presentation in the case of logic programming) which works by extracting a program from a constructive proof of a speci cation formula. Thus, in the proofs as programs approach, programs synthesis is regarded as a theorem proving activity, whereas by using our unfold fold method we view ....

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J. W. Lloyd, editor, Computational Logic, Symposium Proceedings, Brussels, November

....Of course, some semantics preserving transformations of the logic program will normally still be necessary to produce a useful decompiler in practice. The compiler presented here has been rigorously developed, but ongoing research into the synthesis of logic programs from inductive proofs [26] and also the study of termination of logic programs [27] could ensure even more confidence in the correctness of the compiler. The scalability of such approaches will be important if they are to be used in practice. Despite the fact that generated instructions are optimised in length, much ....

Bundy A, Smaill A, Wiggins G. The Synthesis of Logic Programs from Inductive Proofs. In: Lloyd, JW (ed) Computational Logic. Springer-Verlag, 1990, pp 135--149 (Basic research series)

....A very large number of synthesis methods have been proposed in the literature. All these methods may vary because of: i) the form of the initial speci cation, ii) the rules used for deriving programs from speci cations, and (iii) the language used for the synthesized programs (see, for instance, [28, 59, 69, 85] for references in the case of logic programs) Our synthesis method is related to the methods for logic program synthesis (see, for instance, 85] where the initial speci cation is an equivalence formula of the rst order predicate calculus and one is allowed to use derivation rules similar to ....

....Thus, no implicit de nitions like those provided by formulas of the form (1) above are allowed. Our synthesis method can also be viewed as a technique for the extraction of a program from an unfold fold proof. Thus, the basic idea of our method is also related to the proofs asprograms approach [7, 28, 69, 107] whereby the constructive proof of a property can be used for synthesizing a program which satis es that property. However, between our approach and the proofs as programs approach, there are many di erences. Among them we recall the di erences 54 due to: i) the derivation rules considered (in ....

[Article contains additional citation context not shown here]

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J. W. Lloyd, editor, Computational Logic, Symposium Proceedings, Brussels, November 1990, pages 135149, Berlin, 1990. Springer-Verlag.

....synthesize a program and spec is any formula of the rst order predicate calculus which provides the speci cation of the predicate newp. The unfold fold rules can indeed be viewed as derivation rules in these synthesis methods. Our synthesis method is also related to the proofs as programs method [1, 7, 12, 23] whereby the constructive proof of a property of the form 8X 9Y spec(X; Y ) can be used for synthesizing a program which, for any input X , computes an output Y such that spec(X; Y ) holds. The main di erence between our method and the ones we have mentioned above is that we allow for a more ....

....A very large number of synthesis methods have been proposed in the literature. All these methods may vary because of: i) the form of the initial speci cation, ii) the rules used for deriving programs from speci cations, and (iii) the language used for the synthesized programs (see, for instance, [7, 11, 12, 16] for references in the case of logic programs) Our synthesis method is related to the methods for logic program synthesis (see, for instance, 16] where the initial speci cation is an equivalence formula of the rst order predicate calculus and one is allowed to use derivation rules similar to ....

[Article contains additional citation context not shown here]

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J. W. Lloyd, editor, Computational Logic, Symposium Proceedings, Brussels, November 1990, pages 135-149, Berlin, 1990. Springer-Verlag.

....et al. 93] and has been rather successfully used in the automatic planning [Bundy 88] of inductive proofs in a functional framework. Conventional rippling 2 has also been applied in logic program synthesis and transformation by means of the proofs as programs approach [Bates Constable 85, Bundy et al. 90, Wiggins 92b] However, the relational nature of logic programming pinpoints the weakness of conventional rippling for dealing with relational expressions. Conventional rippling makes an extensive use of information contained in the syntactic structure of a functional expression. Conventional ....

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135-- 149. Springer-Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Research Paper 501.

....applications of it will be investigated. First, we will go back to the problem of deriving correct Prolog implementations of purely declarative descriptions. More specifically, we will investigate various logic description (or program) classes which can be obtained by inductive [34] or deductive [11, 35, 42, 68] synthesis. Following the general idea of [32] we will investigate how our analyser can be used to prove that some Prolog translation of such logic descriptions correctly implements the intended meaning of the descriptions according to the correctness criteria proposed by the authors of [34, 35] ....

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Computational Logic, Esprit Basic Research Series, 1990.

....predicate for which we want to synthesize a program and spec is any formula of the first order predicate calculus. The unfold fold rules can indeed be viewed as derivation rules in these synthesis methods. The basic idea of our synthesis method is also related to the proofs asprograms paradigm [1, 7, 12, 23] whereby the constructive proof of a property of the form 8X 9Y spec(X; Y ) can be used for synthesizing a program which, for any input X , computes an output Y such that spec(X; Y ) holds. However, the main difference between our method and the two above mentioned ones is that we allow for a more ....

....very large number of synthesis methods have been proposed in the literature. All these methods may vary because of (i) the form of the initial specification, ii) the rules used for deriving programs from specifications, and (iii) the language used for the synthesized programs (see, for instance, [7, 11, 12, 16] for references in the case of logic programs) Our synthesis method is related to the methods for logic program synthesis (see, for instance, 16] where the initial specification is an equivalence formula of the first order predicate calculus and one is allowed to use derivation rules similar to ....

[Article contains additional citation context not shown here]

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J. W. Lloyd, editor, Computational Logic, Symposium Proceedings, Brussels, November 1990, pages 135--149, Berlin, 1990. Springer-Verlag.

.... to build logic programs by theorem proving where the program is originally left unspecified as a higher order meta variable and is filled in incrementally during the resolution steps; the use of resolution is similar to the use of middle out reasoning to build logic programs as demonstrated in [20, 21, 6, 33]. Isabelle manipulates objects of the form 3 [ F1; Fn ] F. A proof proceeds by applying rules to such formulas which result in zero or more subgoals, possibly with different assumptions. When there are no subgoals, the proof is complete. Although Isabelle proof rules are formalized ....

....notion of equivalence we use is equivalence between the specification and a logic program represented as a pure logic program in the above theory. Pure logic programs themselves are equivalences between a universally quantified atom and a formula in a restricted subset of first order logic (see [6] for details) they are similar to the logic descriptions of [12] For example, the following is a pure logic program for list membership, where . is cons. 4 8x y:p(x; y) x = F alse) 9v 0 v 1 :x = v 0 :v 1 (y = v 0 p(v 1 ; y) 1) Such programs can be translated to Horn clauses or ....

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135--149. Springer-Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Re search Paper 501.

....automated synthesis, but rather for interactive synthesis, so as to cope with incompleteness. Examples give rise to inductive synthesis (generalization [5] 6] 7] learning [8] 9] whereas axiomatic specifications (and thus properties) give rise to deductive synthesis (proofs as programs [10], 11] 12] rewriting [13] 14] 15] Since we have both specification types, we want to avoid using only one kind of inference, and thus degrading the non used information source into validation information. We shall therefore strive for inductive and deductive synthesis, using whichever ....

.... . L= HL TL] compress(TL,TCL) TCL= HL,M TTCL] CL= HL,s(M) TTCL] HL=b TL= b] TCL= b,1 ] HL=e TL= e,e] TCL= e,2 ] HL=f TL= f,g] TCL= f,1 , g,1 ] Figure 7 LD 6 (compress) The first task is done using a Proofs as Programs Method (see [10], 11] 12] instantiations of the Discriminate k are extracted from the proof that: g(LD 6 (r) P(r) The second task is heuristic driven, i.e. after applying some generalization heuristics, we postulate that the resulting discriminators are the intended ones. Some theoretical aspects ....

Bundy A, Smaill A and Wiggins G. The Synthesis of Logic Programs from Inductive Proofs. In: Lloyd JW (ed) Computational Logic. Springer Verlag, 1990, pp 135149.

....approach, the specification takes the form of a theorem (or more accurately a conjecture) stating the existence of the required output for any legitimate input; a (successful) constructive proof of this theorem then yields a program that is correct with respect to the specification. See [1, 2] for instance. A more direct approach is to give the specification in the form of a set of axioms, and then to systematically derive a set of clauses which are logical consequences of these axioms. We shall call this approach deductive synthesis. 1 Examples include [5, 6, 9] In this paper, we ....

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Proc. Esprit Symposium on Computational Logic, pages 135--149. Springer-Verlag, 1990.

....but is formally verified and very simple to understand. In [20] Whelk is presented as a new kind of logic where specifications are manipulated in a special kind of tagged formal system. A tagged formula A is of the form [ A] P (x) OE . 1 The tag subscript represents a pure logic program [4] where P is an atom and OE a formula in a restricted subset of first order logic. The Whelk logic manipulates these tags so that the tagged (subscripted) program should satisfy two properties. First, the tagged program should be logically equivalent to formula it tags in the appropriate ....

....are also included: the published Whelk rules, the derived IsaWhelk rules, and the entire proof script for the subset proof. 2 Background to Interpretation Due to space considerations I only give very brief overviews of Whelk and Isabelle. Details on Whelk are found in [20] 2 (see also [4]) and on Isabelle in [14, 15, 16, 17] 2.1 Overview of Whelk The following summarizes [20] Whelk is a sequent calculus implemented in Prolog. Its logical basis is constructive sorted first order logic with equality, extended with an operator and rules for reasoning about . Whelk proofs ....

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135--149. Springer-Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Re search Paper 501.

....as control, operational correctness, and efficiency) of software. This distinction is often blurred by the promises of Logic Programming, promises that have however not been fulfilled by languages such as Prolog. It is but a recent trend to dissociate algorithms and programs in Logic Programming [16] [24] 32] 56] 86] This corresponds to recasting Kowalski s equation Algorithm = Logic Control [55] as Program = Algorithm Control . Since there is no consensus yet on these issues, and in order to keep our terminology simple, the word algorithm stands in the sequel for algorithm or ....

....unknown or to change over time. Constructive Synthesis (also known as Proofs as Programs Synthesis) an algorithm is extracted from a (sufficiently) constructive proof of the satisfiability of the specification. Sample works are those of T rnlund et al. 29] 46] Takayama [83] Bundy et al. [16], Wiggins [86] Fribourg [35] and so on. These two categories are not as clear cut as one might think, as some synthesis mechanisms can be successfully classified in the two of them [56] The two approaches are probably only facets of the same technique. A third category, namely Schema guided ....

Alan Bundy, Alan Smaill, and Geraint Wiggins. The synthesis of logic programs from inductive proofs. In J. W. Lloyd (editor), Proceedings of the ESPRIT Symposium on Computational Logic, pages 135--149. Springer-Verlag, 1990.

....structural induction. These programs are recursive, and though correct not obviously logical consequences of the pre and postconditions of the predicate. 1 Introduction Recently there has been much interest in constructive methods to derive logic programs from their specifications (e.g. Bundy et al. 90] Flener 91] Fribourg 90] Deville 90] Lau, Prestwich 91] Bundy and collaborators [Bundy et al. 90] in their Oyster system synthesize programs in first order logic from non executable specifications in typed constructive logic. The synthesis uses the proofs as programs technique which ....

....of the pre and postconditions of the predicate. 1 Introduction Recently there has been much interest in constructive methods to derive logic programs from their specifications (e.g. Bundy et al. 90] Flener 91] Fribourg 90] Deville 90] Lau, Prestwich 91] Bundy and collaborators [Bundy et al. 90] in their Oyster system synthesize programs in first order logic from non executable specifications in typed constructive logic. The synthesis uses the proofs as programs technique which constructively proves a specification theorem: each proof step is associated with a program construction step, ....

[Article contains additional citation context not shown here]

A.Bundy, A. Smaill, G. Wiggins, The Synthesis of Logic Programs from Inductive Proofs, in: J. W. Lloyd (ed.), Computational Logic, ESPRIT Symposium Proceedings, Brussels November 1990, Springer, 1990

....mathematics. Quine [Quine 70] defines as constructive a mathematics which is intolerant of methods affirming the existence of things of some sort without showing how to find them. Constructive methods especially constructive logics are also proposed by other researchers ( Bry 89] Bundy et al. 90] Deville 90] Flener 91] Fribourg 90] Lau, Prestwich 91] 4.4 Degree of Abstraction of the Specification Borrowing a saying of Einstein s, I maintain that specifications should be as abstract as possible, but not more abstract. I see three limitations to the degree of abstraction. First, ....

A. Bundy, A. Smaill, G. Wiggins, The Synthesis of Logic Programs from Inductive Proofs, in J. W. Lloyd (Ed.), Computational Logic, Symposium Proceedings, Brussels November 1990, Springer, 1990

....of an input output theorem of the form 8x9y r(x; y) 14) From a proof of this theorem, a program to compute r can be extracted. In logic programming, however, the connection between deductive and constructive synthesis is particularly close. For example, in the constructive synthesis method of [2], the input output relation r(x; y) in (14) is itself an if and only if specification. In [14, 6] program extraction is performed by proving goals of the form 8x9y q(x; y) r(x) 15) using an extended Prolog execution mechanism. Here, r(x) can be regarded as an input, and q(x; y) as an output. ....

A. Bundy, A. Smaill and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Proc. Esprit Symposium on Computational Logic, pages 135--149, Springer-Verlag, 1990.

....condition, i.e. for every input x there is at least one y which satisfies r(x; y) and is computed by the specified (or extracted) program. In logic programming, the connection between deductive and constructive synthesis is particularly close. For example, in the constructive synthesis method of [2], the input output relation r(x; y) in (18) is itself an iff specification. In [15, 7] program extraction is performed by proving goals of the form 8x9y . q(x; y) r(x) 19) using an extended Prolog execution mechanism. Here, r(x) can be regarded as an input, and q(x; y) as an output. ....

A. Bundy, A. Smaill and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Proc. Esprit Symposium on Computational Logic, pages 135--149, Springer-Verlag, 1990.

....semantics of Prolog (Lloyd, 1987) may be assumed to hold and it would be possible to perform a formal proof of the correctness of the Prolog compiler and decompiler which are presented here. For example, the approach of program synthesis using the proofs as programs technique presented in (Bundy et al. 1990) could be (somewhat laboriously) applied. Research is very active in the area of logic program synthesis and transformation (Clement et al. 1991) Less pure features used in the code presented here include var, nonvar, integer, assert and retract, but these are used in a very restricted manner ....

Bundy, A., Smaill, A. and Wiggins, G. (1990). `The Synthesis of Logic Programs from Inductive Proofs', in Lloyd, J.W. (Ed.), Computational Logic, SpringerVerlag, Basic Research Series, 135--149.

....(not included in the paper) consist of about two pages of program code. Thus, it would be tractable to formally prove the prototype compiler implements the specification for a given set of inputs, assuming a suitable semantics of (a subset of) Prolog [Llo87] if this is of concern (e.g. see [BSW90]) In addition, optimization using transformation of logic programs [ClL92] would be possible. However this has not (yet) been attempted by the authors, since the prototype has simply been used as a means of quickly animating the specification mechanically. Proofs of termination and non violation ....

Bundy, A., Smaill, A. and Wiggins G.: The Synthesis of Logic Programs from Inductive Proofs. In Lloyd, J. W. (ed.) Computational Logic. Springer-Verlag, Basic research series, pp. 135--149, 1990.

....synthesis of lowcomplexity algorithms possible, if not likely, rather than a mere pot shot. In this paper, I explore these issues in the logic programming framework, and focus on the concept of logic algorithm, as originally introduced by Deville [19] 20] and later also advocated by others [10] [11] [43] 74] Informally, a logic algorithm is an algorithm expressed in (first order) logic. For pragmatic reasons (for example, the ease of implementation into Prolog programs) I propose the following more restrictive formal definition: Definition 1: A logic algorithm defining a predicate r n, ....

Alan Bundy, Alan Smaill, and Geraint Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd (ed), Proc. of the ESPRIT Symposium on Computational Logic, pp. 135--149. Springer-Verlag, 1990.

....can t completely specify a problem) Axiomatizations of a problem in (some subset of) first order logic, e.g. firstPlateau(List,Plateau,Suffix) append(Plateau,Suffix,List) allEqual(Plateau) break(Plateau,Suffix) lead to synthesis based on deductive inference. The systems of, e.g. (Bundy et al. 1990), Fribourg, 1990) Wiggins, 1992) perform proofs as programs synthesis: programs are extracted from constructive proofs of the satisfiability of specifications. The systems of, e.g. Clark, 1981) Hansson, 1980) Hogger, 1981) Lau and Prestwich, 1990) perform transformational synthesis: ....

Bundy, A., Smaill, A., Wiggins, G. (1990). The synthesis of logic programs from inductive proofs. In: Lloyd, J.W. (ed) Computational Logic. Springer-Verlag, 1990, pp 135-149.

....of equivalence. In our work, we have formalized logic programs in two different ways. First, as firstorder formulae in a restricted language (see x3.1 and x3.2) where each program is associated with a set of formulae that define it for different possible inputs. This formalism is that used by Bundy, Smaill and Wiggins (1990) and is similar to the logic descriptions of Flener and Deville (1991) Second, as Horn clauses (see x3.3) which constitute an inductive definition. We have also explored different notions of equivalence. With respect to the first formalization we have viewed equivalence as provable equivalence ....

Bundy, A., Smaill, A., Wiggins, G. A. (1990). The synthesis of logic programs from inductive proofs.

....here is to automate the synthesis of logic programs. This is done by adapting techniques from areas such as middle out reasoning in explicit proof plans [Bundy 88, Bundy et al. 90a] proofs as programs [Bates Constable 85] and deductive synthesis [Bibel 80] We synthesize pure logic programs [Bundy et al. 90b] from specifications in sorted, first order theories. The approach encompasses two levels of reasoning: An object level, which is a sorted, first order predicate logic with equality, and a meta level, which reasons explicitly with object level proofs. At the object level, we prove that the ....

....proof development systems for a variant of Martin Lof type theory[Martin Lof 79] Adapting proofs as programs to logic program synthesis is not straightforward. The main problem is that proofs as programs synthesizes total functions. Logic programs, however, are partial and multivalued [Bundy et al. 90b] They may return no value, i.e. fail, or they may return more than one value on backtracking. Moreover, they may not terminate. One adaptation of proofs as programs to logic program synthesis is presented in [Fribourg 90] Fribourg synthesizes programs from Prolog style proofs. He extends ....

[Article contains additional citation context not shown here]

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135--149. Springer-Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Research Paper 501.

....such a member. Since terms in the calculus can be evaluated, proofs give rise to functional programs. Adapting proofs as programs to logic program synthesis is not straightforward. The proofs as programs approach synthesizes total functions, whereas logic programs are partial and multivalued [Bundy et al. 90b] Logic programs may return no value, i.e. fail, or they may return more than one value on backtracking. Moreover, they may not terminate. One adaptation of proofs as programs to logic program synthesis is presented in [Fribourg 90] Fribourg synthesizes programs in Prolog style proofs. He ....

....in terms of x Gamma . However, the program will only be correct when the variables in x Gamma are ground and the variables in y Gamma are unbound. Also, it will return only one answer. It is thus a functional program in the guise of a logic program. To overcome these disadvantages, Bundy et al. 90b] suggests viewing logic programs in all ground mode as functions returning a boolean value. Specifications of logic programs are thus of the form: 8args Gamma Gamma Gamma Gamma : 9boole: spec(args Gamma Gamma Gamma Gamma ) boole The programs resulting from proofs of such ....

[Article contains additional citation context not shown here]

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135--149. Springer-Verlag, 1990. Esprit Basic Research Series. Also Edinburgh DAI Research Paper 501.

....A Survey Deville and Lau [3] also contains a brief survey of logic program synthesis methods. In this tutorial, we shall follow their style, and for each approach, we shall explain it with an example: ffl For constructive synthesis, we shall base our description on the work by Bundy and Wiggins [1]. ffl For deductive synthesis, we follow that of Lau and Ornaghi [8] For transformational synthesis by fold unfold, we will describe the work of Sato and Tamaki [11] For transformational synthesis by partial deduction, we will describe the work of Komorowski [7] Transformational synthesis ....

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Proc. ESPRIT Symposium on Computational Logic, pages 135--149. Springer-Verlag, 1990.

....step is simplifying a wave front. 3 Middle Out Synthesis 3.1 Pure Logic Programs The logic programs we synthesize are the completions of a subset of normal programs (see Lloyd [Lloyd 87] which we call pure logic programs. They are similar to pure logic programs as defined by Bundy et al. in [Bundy et al. 90b] and the logic descriptions of Deville [Deville 90] Formally, we define them as finite sets of pure logic program clauses. A pure logic program clause is a closed, typed formula of the form 8x : T : A(x) H where x is a vector of distinct variables with types given by T (generally left ....

....One of our aims was to improve on the results achieved by known synthesis systems, particularly in terms of automation and selection of induction schemes. Three examples from the literature are of special importance: subset from Lau and Prestwich [Lau Prestwich 88] delete from Bundy et al. [Bundy et al. 90b] and qr from Biundo [Biundo 89] For the first two examples, the aim was to fully automate the synthesis, which, in the literature, was semi automatic or interactive. For the last example, the aim was to synthesize a better algorithm by finding a more appropriate induction. Periwinkle is able to ....

[Article contains additional citation context not shown here]

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135--149. Springer-Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Research Paper 501.

....there are potentially many or no outputs. A solution to those problems is to consider only the all ground directionality. The predicate can then be seen as a boolean valued function. This is the key idea to transform proofs as functional programs into proofs as relationalprograms [Bundy et al. 90a] The form of a synthesis conjecture to prove is largely a matter of taste. In Whelk a new operator, has been introduced with the meaning It is decidable whether: Wiggins et al. 91, Wiggins 92] With this operator, to synthesize a program with vector of arguments a Gamma of type ....

....this proof critic, but it has been proved useful in a synthesis of the subset 2 predicate. 4 Application: The delete Predicate Synthesis We will now give an example of the application of those methods to a simple problem: the synthesis of the delete predicate (this proof was done by hand in [Bundy et al. 90a] To simplify the reading, the type information used in Whelk will be omitted in the equations, and the hypothesis list will not always be fully rewritten. This should not cause any misunderstanding. We start, as explained in section 2.1, with the synthesis conjecture: 8Old: 8X: 8New: ....

A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic, pages 135--149. SpringerVerlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Research Paper 501.

No context found.

Bundy, A., Smaill, A. and Wiggins, G.: The Synthesis of Logic Programs from Inductive Proofs. In J. W. Lloyd (ed.) Proceedings of Esprit Symposium on Computational Logic, pp. 135-149. Springer-Verlag, 1990.

No context found.

A. Bundy, A. Smaill, and G. Wiggins, "The Synthesis of Logic Programs from Inductive Proofs," in J. W. Loyd (ed), Proceedings of the ESPRIT Symposium on Computational Logic , pp. 135-149, Springer-Verlag, 1990.

No context found.

A. Bundy, A. Smaill, and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Proc. Esprit Symposium on Computational Logic, pages 135--149. Springer-Verlag, 1990.

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.