L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D. H. D. Warren and P. Szeredi, editors, Proceedings Seventh International Conference on Logic Programming, Jerusalem, Israel, June 18-20,  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....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 ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D. H. D. Warren and P. Szeredi, editors, Proceedings Seventh International Conference on Logic Programming, Jerusalem, Israel, June 18-20,

....spec(i) b 7 Proving a speci cation of this type in a constructive logic yields a function which can be interpreted as a logic program. A user guided implementation of this system was created called Whelk. This technique works for relations which are decidable. Another approach is given in [Fribourg 90] Deductive Synthesis Deductive synthesis starts with a speci cation and then applies a number of inference rules to arrive at a program. In [Lau Prestwich 90] Lau and Prestwich synthesize programs which are speci ed as folding problems by deductive synthesis. A folding problem is a speci ....

L. Fribourg. Extracting logic programs from proofs that use extended prolog execution and induction. In Proceedings of 7th Int. Conf. on Logic Programming, pages 685-699. MIT press, 1990.

....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]

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D. H. D. Warren and P. Szeredi, editors, Proceedings Seventh International Conference on Logic Programming, Jerusalem, Israel, June 18-20, 1990, pages 685699. The MIT Press, 1990.

....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]

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D. H. D. Warren and P. Szeredi, editors, Proceedings Seventh International Conference on Logic Programming, Jerusalem, Israel, June 18-20, 1990, pages 685-699. The MIT Press, 1990.

....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 standard Prolog goals to goals of the form 8x Gamma :9y Gamma : q(x Gamma ; y Gamma ) r(x Gamma ) where q(x Gamma ; y Gamma ) and r(x Gamma ) are conjunctions of atoms, and he extends standard ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proceedings of Eighth International Conference on Logic Programming, pages 685 -- 699. MIT Press, June 1990.

....be used for program verification. A companion paper by Kanamori and Fujita [10] analyzed several techniques for the formulation of induction schemata and showed how two or more such schemata could be merged into one. These ideas have been extended and refined in a series of papers by Fribourg [4, 5, 6]. Other contributions include the work of Hsiang and Srivas [9] and Elkan and McAllester [3] The biggest problem in all of this work seems to be: How to conjecture an appropriate induction schema In this extended abstract, we will show how to formulate induction schemata in secondorder ....

L. Fribourg. Extracting logic programs from proofs that use extended PROLOG execution and induction. In Logic Programming: Proceedings of the Seventh International Conference, pages 685--699. MIT Press, 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]

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D. H. D. Warren and P. Szeredi, editors, Proceedings Seventh International Conference on Logic Programming, Jerusalem, Israel, June 18-20, 1990, pages 685--699. The MIT Press, 1990. 49

....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 inference ....

.... . 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 of this ....

Fribourg L. Extracting Logic Programs from Proofs that Use Extended Prolog Execution and Induction. In: Proceedings of ICLP-90, MIT Press, Cambridge (MA, USA), 1990, pp 685-699.

....independent of the way (mode) the resulting program can be used. Examples give rise to inductive synthesis (generalization ( Sum77, BS79, Bie84] learning ( Sha82, Tin90, Mug92] whereas axiomatic specifications (and thus properties) give rise to deductive synthesis (proofs as programs ( [MW79, BSW90, Fri90]) transformations ( Han80, Cla81, Hog81, LP90] Since we have both kinds of specification information, we want to avoid using only one kind of inference, and thus degrading the non used information source into validation information. We therefore strive for inductive and deductive synthesis, ....

....by discriminate k such that it is partly defined by the following clause: discriminate k (HX,TX,y)oe ki Body i oe ki where Body i is the body of property P i , and where y is the value of Y in the head of P i . Note that this is not like classical program extraction from proofs (compare with [BSW90, Fri90, MW79]) since the program is here extracted from the unique final result of the proof, rather than on the fly (or a posteriori) from multiple intermediate proof steps. A derivation fails iff it doesn t succeed. Nothing is done in that case. Failure is of course not always detectable, since an infinite ....

L. Fribourg. Extracting Logic Programs from Proofs that Use Extended Prolog Execution and Induction. In D.H.D. Warren and P. Szeredi, editors, Proc. Seventh International Conference on Logic Programming, Series in Logic Programming, pages 685--699, Jerusalem, Israel, June 1990. The MIT Press.

....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 extends standard Prolog goals to implicational goals of the form 8x Gamma : 9y Gamma : q(x Gamma ; y Gamma ) r(x Gamma ) where q(x Gamma ; y Gamma ) and r(x Gamma ) are conjunctions of atoms. He also ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proceedings of Eighth International Conference on Logic Programming, pages 685 -- 699. MIT Press, June 1990.

..... 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 Synthesis, should be added: an ....

Laurent Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D. H. D. Warren and P. Szeredi (editors), Proceedings of ICLP'90, pages 685--699. The MIT Press, 1990. Updated and revised version in [50], pages 39--66.

....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 constructively proves a ....

L. Fribourg, Extracting logic programs from proofs that use extended Prolog execution and induction, in: Proceedings 7th International Conference on Logic programming, MIT Press, 1990

....to running conjunctive partial deduction alone. Work very much related to RAF is [15] which provides some pragmatics for removing unnecessary variables in the context of optimising binarised Prolog programs. Another related technique is truncation of Prolog programs derived by extended execution [19]. In some cases truncation is more powerful than RAF, but in order to apply it (soundly) one has to prove termination of the runtime goal and functionality of the goal to be truncated. Techniques similar to RAF have also appeared in functional programming, e.g. Chin [13] describes a technique to ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. Proceedings ICLP'90, 685--699, MIT Press, 1990.

....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 specification as an adequate ....

L. Fribourg, Extracting logic programs from proofs that use extended Prolog execution and induction, in: Proceedings 7th International Conference on Logic programming, MIT Press, 1990

....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. Therefore, 15) is also closely related to our conditional specification. Selector specifications ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D.H.D. Warren and P. Szeredi, editors, Proc. 7 th Int. Conf. on Logic Programming , pages 685--699, MIT Press, 1990.

....such family derived in the literature. The ability to derive these procedures from a common specification is a promising result for our system, and moreover it gives us a neat taxonomy of these sorting algorithms (see [10, 11] Furthermore, compared to recent work in logic program synthesis (e.g. [6, 15, 16]) our system seems to be the only one that has been applied successfully to the synthesis of large families of nontrivial procedures. Also, our synthesis of procedures for the distributive sorting algorithms, radix exchange sort and distribution sort , and the block sorting algorithms, external ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D.H.D. Warren and P. Szeredi, editors, Proc. 7 th Int. Conf. on Logic Programming, pages 685--699. MIT Press, 1990.

....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. Therefore, 19) is similar to a selector specification of the form: r(x) q P (x; y) q(x; y) ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D.H.D. Warren and P. Szeredi, editors, Proc. 7 th Int. Conf. on Logic Programming , pages 685--699, MIT Press, 1990.

....Work in Program Synthesis Most program synthesis approaches have originated in the field of functional programming. There has, however, been increased interest in adapting these to logic program synthesis. For a detailed overview of logic program synthesis, see [Deville Lau 94] Fribourg [Fribourg 90] and Wiggins [Wiggins 92] both adapt the proofs as programs approach to logic program synthesis. Fribourg, however, uses 89 specifications. The synthesized programs are thus not truly relational. Wiggins develops a synthesis logic for relational program synthesis with a decidability operator, ....

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proceedings of Eighth International Conference on Logic Programming, pages 685 -- 699. MIT Press, June 1990.

....could be constructed automatically. Other work in inductive theorem proving and logic programming such as, for example [3, 12, 26] should be applicable in our setting to aid in the construction of such transformations. Closely related to the ideas presented here is work by Fribourg [9] in the simpler setting of Horn clauses. Again, his ideas could add to the degree of automation available within our methodology. The remainder of this paper is organized as follows: In Section 2 we present some of the basic ideas behind Elf, schema checking, and its connection to proof by ....

....in this paper, the latter choice is a very natural one, and many examples can be treated very elegantly. Moreover, it does not preclude the application of automated theorem proving methods, as they can be used to synthesize schematic relations. This is one of Fribourg s basic observations [9] and illustrated in Section 3. But even without any automatic assistance beyond term reconstruction it is feasible to demonstrate non trivial meta theorems. We now return to the example. The induction principle for objects constructed over the given signature is just the familiar induction ....

Laurent Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In David H.D. Warren and Peter Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 685--699. MIT Press, June 1990.

....to develop programs in procedural programming languages to produce clear, well structured code. There is no analogous method for the systematic construction of Prolog programs. Sporadic attempts have been made over the years to automatically systematically construct logic programs, for example [LP90, Fri90]. However, much of the effort has been concentrated on logic and formal transformations. Our experience in teaching Prolog suggests that students do not naturally develop programs by developing and then transforming correct statements of logic. Rather, they think of programming in procedural ....

L. Fribourg. Extracting logic programs from proofs that use extended prolog execution and induction. In P. Szeredi and D. H. Waren, editors, Proceedings of the Seventh International Conference on Logic Programming, Cambridge, USA, November 1990. MIT Press.

....0 ,M 0 ) minmax( NjY] L,M) L 0 N, M 0 N, L=N, M=N, minmax(Y,L 0 ,M 0 ) minmax( NjY] L,M) L 0 N, M 0 N, L=N, M=M 0 , minmax(Y,L 0 ,M 0 ) 3. 2 Projection The operation of projection consists in dropping one (or more) argument in the definition of recursive predicates [15, 11]: here the dropped argument is the list Y. We have definition and lemma 3.2 Consider an orderly list recursive predicate p defined by the following program f p( X) a i (X) g i2I f p( NjY] X) b j (X,N,X 0 ) p j (Y,X 0 j ) g j2J f p( NjY] X) c k (X,N,X 0 ) p(Y,X 0 ) g k2K ....

Fribourg, L. (1990). "Extracting Logic Programs from Proofs that Use Extended Prolog Execution and Induction", Intl. Conf. on Logic Programming, MIT Press, pp. 685-699.

....contained in the extracted program. We describe how to synthesize Prolog procedures when applying the inference rule and show that they are guaranteed to preserve partial correctness and termination. A comparison is made between the new rule and the rules of Restricted Structural Induction [Fri 90] and Computation Induction [Cla 79] and we note that by an uncomplicated preprocessing of the goal formula and the program the new rule subsumes the two latter rules. 1 Introduction Consider the predicate p(X) defined by the Prolog program P , where X is a vector of variables. Suppose we want ....

....from such proofs, we need a framework in wich we can manipulate such formulas and synthesize the associated programs. Extended Prolog Execution [K S 86] provides the proof system needed, and programs can be synthesized during such proofs using a method of Proof Extraction proposed by Fribourg [Fri 90] The plan is as follows. In section 2 we review some formal notions of Extended Prolog Execution and of classical induction rules. In section 3 we introduce the rule of NFI driven Induction. We compare this rule with Structural Induction (section 4) and with Computation Induction (section 5) We ....

[Article contains additional citation context not shown here]

Fribourg L., Extracting Logic Programs from Proofs that use Extended Prolog Execution and Induction. Proc. 7th Intl. Conf. on Logic Programming, Jerusalem, 1990, pp. 685-699.

No context found.

L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proc. 7 th Int. Conf. on Logic Programming, pages 685--699. MIT Press, 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.