Synthesis and transformation of logic programs using unfold/fold proofs Export

@article{citeulike:6002407, abstract = {We present a method for proving properties of definite logic programs. This method is called unfold/fold proof method because it is based on the unfold/fold transformation rules. Given a program P and two goals (that is, conjunctions of atoms) and , where , , and are pairwise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula }, author = {Pettorossi, A.}, citeulike-article-id = {6002407}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/S0743-1066(99)00029-1}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S0743-1066(99)00029-1}, doi = {10.1016/S0743-1066(99)00029-1}, issn = {07431066}, journal = {The Journal of Logic Programming}, keywords = {fold-unfold, logic-programming, program-transformation}, month = {December}, number = {2-3}, pages = {197--230}, posted-at = {2009-10-24 20:44:55}, priority = {2}, title = {Synthesis and transformation of logic programs using unfold/fold proofs}, url = {http://dx.doi.org/10.1016/S0743-1066(99)00029-1}, volume = {41}, year = {1999} }

TY - JOUR ID - citeulike:6002407 L3 - citeulike-article-id:6002407 N2 - We present a method for proving properties of definite logic programs. This method is called unfold/fold proof method because it is based on the unfold/fold transformation rules. Given a program P and two goals (that is, conjunctions of atoms) and , where , , and are pairwise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula IS - 2-3 JF - The Journal of Logic Programming SN - 07431066 EP - 230 TI - Synthesis and transformation of logic programs using unfold/fold proofs VL - 41 SP - 197 KW - fold-unfold KW - logic-programming KW - program-transformation AU - Pettorossi, A PY - 1999/12// UR - http://dx.doi.org/10.1016/S0743-1066(99)00029-1 ER -