Alberto Pettorossi and Maurizio Proietti. Transformation of logic programs. In D. M. Gabbayand, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 697--787. Oxford University Press, 1998.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....reasoning with the deductive process, so that the derived program is guaranteed to be correct. Unfortunately, it is known that the deductive process alone (i.e. unfolding) does not generally suce for coming up with the corrected program, and inductive generalization techniques are necessary [15, 34, 35]. In [23, 24, 20] a bottom up framework for synthesizing correct functional logic programs (w.r.t. the ground success set, Herbrand semantics) is presented which induces program rules from sets of equations which are respectively incorrect and correct w.r.t. the pursued program. Their ....

A. Pettorossi and M. Proietti. Transformation of Logic Programs. In Handbook of Logic in Arti cial Intelligence, volume 5, pages 697-787. Oxford University Press, 1998.

....more recently that approach has been applied by Seki to logic programs with negation in the bodies of the clauses [Sek91] Di erent sets of transformation rules have been proposed in the literature for the di erent classes of programs which have been considered. The interested reader may refer to [PeP98] for a survey. We will focus our attention on logic program transformation. This choice is motivated by the fact that in Correspondence and o print requests to: Maurizio Proietti, IASI CNR, Viale Manzoni 30, I 00185 Rome, Italy. e mail: proietti iasi.rm.cnr.it A. Pettorossi and M. Proietti logic ....

A. Pettorossi and M. Proietti. Transformation of logic programs. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Arti cial Intelligence and Logic Programming, volume 5, pages 697-787. Oxford University Press, 1998.

....more recently that approach has been applied by Seki to logic programs with negation in the bodies of the clauses [Sek91] Di erent sets of transformation rules have been proposed in the literature for the di erent classes of programs which have been considered. The interested reader may refer to [PeP98] for a survey. We will focus our attention on logic program transformation. This choice is motivated by the fact that in Correspondence and o print requests to: Maurizio Proietti, IASI CNR, Viale Manzoni 30, I 00185 Roma, Italy. e mail: proietti iasi.rm.cnr.it A. Pettorossi and M. Proietti ....

A. Pettorossi and M. Proietti. Transformation of logic programs. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Articial Intelligence and Logic Programming, volume 5, pages 697-787. Oxford University Press, 1998.

....5.1 For every predicate p in P M(varterm(P) p) M(P) p) Proof: Consider the transformations 1 to 6. By unfolding the right hand side of 1 to 6 with the unit clauses for predefined predicates, the clauses of the left hand side are regained. By the theorem of Tamaki and Sato [22] see also [18], every transformation sequence constructed by unfolding is totally correct with respect to the least Herbrand semantics. 2 5.2 Introduction of Combinator Terms Combinators are now introduced through the following rewriting steps in which is passed from the logical clauses to combilog. This ....

A. Petorossi, M. Proietti, Transformation of Logic Programs. In D. M. Gabbay, C. J. Hogger and J. A. Robinson, eds., Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, forthcoming.

....the variable elimination procedures. The first author was supported by a fellowship from the Japan Society for the Promotion of Science (JSPS) A Transformation Rules Unfold fold transformations for logic programs are first studied by Tamaki and Sato [28] see also Pettorossi and Proietti [19] for a survey paper) The transformation rules are defined as follows. Definition A.1 (definition rule) The definition rule adds a new clause C of the form newp(X 1 ; X k ) A 1 : A n to a given theory where newp=k is a predicate symbol not contained in the theory and A 1 ; A n ....

Alberto Pettorossi and Maurizio Proietti. Transformation of logic programs. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming (Volume 5, Logic Programming), pages 697--787. Clarendon Press, Oxford, 1998.

....to a linearisable program. The class of piecewise linear programs , de ned below, is of special interest, since piecewise linear programs are linearisable [2] In fact, piecewise linear programs can be transformed into linear programs by applying standard program transformation techniques [6], which preserve the least Herbrand model semantics. A piecewise linear program is a Datalog program where in the body of each clause there is at most one atom whose predicate is mutually recursive with the predicate in the head of the clause; a predicate p is mutually recursive with a 3 In ....

.... ; Y ) i 1 (X; X;W;W;Y;Y ) i j;1 (X; X 1 ) r 1 (X; X 1 ) i j;2 (W; W 1 ) r 2 (W; W 1 ) i j;3 (V; V 1 ) r 3 (V; V 1 ) This program is not linear but is piecewise linear and therefore linearisable (see section 2) Note that in this example linearisation can be achieved simply by unfolding away [6] the predicates i j;e , for e = 1; 2; 3: i 0 (X; Y ) i 1 (X; Z; W; U; V; Y ) i 1 (X; Z; W; U; V; Y ) r 1 (X; X 1 ) r 2 (W; W 1 ) r 3 (V; V 1 ) i 1 (X 1 ; Z; W 1 ; U; V 1 ; Y ) i 1 (X; X;W;W;Y;Y ) Example 3.3 Let L = fR i 1 1 R i 2 2 R i 1 3 R 2 4 ji 1 ; i 2 0g (with = fR 1 ; ....

A. Pettorossi and M. Proietti, Transformation of logic programs. Journal of Logic Programming 19/20:261-320 (1994)

....since it requires that the atoms to be folded are next to each other in exactly the same sequence as in the body of the folding clause. This can be solved as we proposed in [14] namely by introducing a further basic transformation operation, the switch one (called also clause rearrangement in [29, 30]) which allows for atoms reordering. Other interesting transformations, which cannot be captured with the previous basic operations alone, deal with linearization of recursion by introducing an accumulator. They make use of the associative property of some predicate, for example the append ....

....strategy we single out conditions under which a replacement is complete and non increasing, namely when we can replace a sequence of atoms by another sequence without losing universal termination. Replacement has been already studied with respect to various declarative semantics (see [12, 13, 21, 26, 29, 30, 35, 37]) We give here a very general definition. Definition 12. Let B 0 be a sequence of atoms defined in P , c : H A;B;C: be a clause in P and let c 0 : H A;B 0 ; C: Let X be the set of common variables and Y be the set of private variables in B and B 0 , namely X = V ar(B) V ar(B 0 ) ....

A. Pettorossi and M. Proietti. Transformation of Logic Programs. In J.A. Robinson editors D.M. Gabbay, C.J. Hogger, editor, Handbook of Logic and Artificial Intelligence. Oxford University Press, 1995.

....from a new specification for adm e . As a subject for future work, it would be interesting to explore the possibility of deriving P rog adm e from the initial, inefficient proof procedure, P rog adm , using standard techniques of logic program transformation (fold, unfold and so on, see [17]) and or techniques borrowed from functional programming (e.g. see [16] Acknowledgements This research was supported by the EEC activity KIT011 LPKRR. The third author was partially supported by EEC HCM Project no CHRX CT93 00414, Logic Program Synthesis and Transformation . The authors are ....

A. Pettorossi, M. Proietti, Transformation of logic programs. Journal of Logic Programming 19/20 (1994), Elsevier, 261--320

.... that of Aravindan and Dung [1] 1 Introduction The standard semantics for definite logic programs (i.e. the least Herbrand model semantics) is preserved by most of the program transformations studied in the literature, in particular by (some forms of) unfolding, folding and goal replacement (see [13] for a summary of these results) This paper provides a methodology for lifting these results from the definite logic program case to the normal logic program case, with respect to stable model [9] partial stable model [15] preferred extension [5] stationary expansion [14] complete scenaria ....

....as follows. First we apply the methodology to prove that the unfolding transformation, reviewed in section 2, preserves all semantics for normal logic programming which can be formulated in argumentationtheoretic terms of [3, 4, 16] The unfolding transformation we consider is adapted from [13]. Section 3 reviews the argumentation framework and the formulation of various normal logic programming semantics in this framework. Section 4 proves that all semantics for normal logic programming formulated in the argumentation framework are preserved by unfolding. Section 5 presents the general ....

[Article contains additional citation context not shown here]

A. Pettorossi, M. Proietti, Transformation of logic programs. Journal of Logic Programming 19/20:261--320 (1994)

....can unify schema based program development with other development methodologies. The use of schemata has sometimes been considered complementary to deductive approaches to program development based on the application of inference rules. These approaches are sometimes called rules strategies (Pettorossi and Proietti, 1998) since development proceeds by applying inference rules possibly guided by high level strategies, which control the development process. By viewing schemata as rules and schema application as logical inference, the distinction between schema based development and development based on ....

Pettorossi, A., Proietti, M. (1998). Transformation of logic programs. In Gabbay, D. M., Hogger, C. J., Robinson, J. A., editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 697--787. Oxford University Press.

....to a linearisable program. The class of piecewise linear programs , defined below, is of special interest, since piecewise linear programs are linearisable [2] In fact, piecewise linear programs can be transformed into linear programs by applying standard program transformation techniques [6], which preserve the least Herbrand model semantics. A piecewise linear program is a Datalog program where in the body of each clause there is at most one atom whose predicate is mutually recursive with the predicate in the head of the clause; a predicate p is mutually recursive with a 3 In ....

.... ) i 1 (X; X;W;W;Y;Y ) i j;1 (X; X 1 ) r 1 (X; X 1 ) i j;2 (W; W 1 ) r 2 (W; W 1 ) i j;3 (V; V 1 ) r 3 (V; V 1 ) This program is not linear but is piecewise linear and therefore linearisable (see section 2) Note that in this example linearisation can be achieved simply by unfolding away [6] the predicates i j;e , for e = 1; 2; 3: i 0 (X; Y ) i 1 (X; Z; W; U; V; Y ) i 1 (X; Z; W; U; V; Y ) r 1 (X; X 1 ) r 2 (W; W 1 ) r 3 (V; V 1 ) i 1 (X 1 ; Z; W 1 ; U; V 1 ; Y ) i 1 (X; X;W;W;Y;Y ) Example 3.3 Let L = fR i 1 1 R i 2 2 R i 1 3 R 2 4 ji 1 ; i 2 0g (with Sigma = fR ....

A. Pettorossi and M. Proietti, Transformation of logic programs. Journal of Logic Programming 19/20:261--320 (1994)

.... programs of a number of e ciency improving transformation strategies for de nite programs presented in the literature, such as strategies for specializing programs, achieving tail recursion, avoiding intermediate data structures, avoiding redundant computations, and reducing nondeterminism (see [53] for a survey) Through some examples, we will indeed show that program e ciency can be improved by applying our unfold fold transformation strategy. The Unfold Fold Transformation Method. Given a locally strati ed program P and a goal G such that vars(G) fX 1 ; Xn g, our ....

.... (rules R1, R5, and R6) The e ectiveness of the unfold fold transformation strategy depends upon the choice of these subsidiary strategies, and much research, mostly in the case of de nite programs, has been devoted to devise subsidiary strategies which allow us to derive very e cient programs [53]. For instance, the introduction of new predicate de nitions, also called eureka de nitions, in uences the e ciency of the derived programs. Various techniques have been proposed for determining the suitable eureka de nitions to be introduced. Here we only want to mention that it is often useful ....

[Article contains additional citation context not shown here]

A. Pettorossi and M. Proietti. Transformation of logic programs. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Articial Intelligence and Logic Programming, volume 5, pages 697787. Oxford University Press, 1998.

No context found.

Alberto Pettorossi and Maurizio Proietti. Transformation of logic programs. In D. M. Gabbayand, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 697--787. Oxford University Press, 1998.

No context found.

Pettorossi, K. and Proietti, M., Transformation of Logic Programs, in: Gabbay, D. M., Hogger, C. J., and Robinson, J. A. (eds.), "Handbook of Logic in Artificial Intelligence and Logic Programming", Vol. 5, Oxford University Press, 1998, pp. 697--787.

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.