Abstract
A framework for unfold/fold transformation of (constraint) co-logic programs has been proposed recently, which can be used to prove properties of co-logic programs, thereby allowing us to reason about infinite sequences of events such as behavior of reactive systems. The main problem with this approach is that only definite co-logic programs are considered, thus representing a rather narrow class of co-logic programs. In this paper we consider ”negation elimination”, a familiar program transformation method, tailored to co-logic programs; given a program for predicate p(X), negation elimination derives a program which computes its negation ¬p(X), when the program satisfies certain conditions. We show that negation elimination can be used for co-logic programs, and its application is correct under the alternating fixpoint semantics of co-logic programs. We show by examples how negation elimination, when incorporated into the previous framework for unfold/fold transformation, allows us to represent and reason about a wider class of co-logic programs. We also discuss the difference between negation elimination applied to co-logic programs and the conventional negative unfolding applied to stratified programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Burstall, R.M., Darlington, J.: A Transformation System for Developing Recursive Programs. J. ACM 24(1), 144–167 (1977)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Colmerauer, A.: Prolog and Infinite Trees. In: Logic Programming, pp. 231–251. Academic Press (1982)
Etalle, S., Gabbrielli, M.: Transformations of CLP Modules. Theor. Comput. Sci., 101–146 (1996)
Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27–44. Springer, Heidelberg (2007)
Gupta, G., Saeedloei, N., DeVries, B., Min, R., Marple, K., Kluźniak, F.: Infinite computation, co-induction and computational logic. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 40–54. Springer, Heidelberg (2011)
Jaffar, J., Stuckey, P.: Semantics of infinite tree logic programming. Theoretical Computer Science 46, 141–158 (1986)
Jaffar, J., Maher, M.J.: Constraint Logic Programming: A Survey. J. Log. Program. 19/20, 503–581 (1994)
Kott, L.: Unfold/fold program transformations. In: Algebraic Methods in Semantics, pp. 411–434. Cambridge University Press (1985)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer (1987)
Lloyd, J.W., Shepherdson, J.C.: Partial Evaluation in Logic Programming. J. Logic Programming 11, 217–242 (1991)
Min, R., Gupta, G.: Coinductive Logic Programming with Negation. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 97–112. Springer, Heidelberg (2010)
Pettorossi, A., Proietti, M.: Transformation of Logic Programs: Foundations and Techniques. J. Logic Programming 19/20, 261–320 (1994)
Pettorossi, A., Proietti, M.: Perfect Model Checking via Unfold/Fold Transformations. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 613–628. Springer, Heidelberg (2000)
Pettorossi, A., Proietti, M., Senni, V.: Deciding Full Branching Time Logic by Program Transformation. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 5–21. Springer, Heidelberg (2010)
Pettorossi, A., Proietti, M., Senni, V.: Transformations of logic programs on infinite lists. Theory and Practice of Logic Programming 10, 383–399 (2010)
Przymusinski, T.C.: On the Declarative and Procedural Semantics of Logic Programs. J. Automated Reasoning 5(2), 167–205 (1989)
Sato, T., Tamaki, H.: Transformational Logic Program Synthesis. In: Proc. FGCS 1984, Tokyo, pp. 195–201 (1984)
Seki, H.: On Inductive and Coinductive Proofs via Unfold/fold Transformations. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 82–96. Springer, Heidelberg (2010)
Seki, H.: Proving Properties of Co-logic Programs by Unfold/Fold Transformations. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 205–220. Springer, Heidelberg (2012)
Seki, H.: Unfold/Fold Transformation of Stratified Programs. Theoretical Computer Science 86, 107–139 (1991)
Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive Logic Programming. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330–345. Springer, Heidelberg (2006)
Simon, L.E.: Extending Logic Programming with Coinduction, Ph.D. Dissertation, University of Texas at Dallas (2006)
Tamaki, H., Sato, T.: Unfold/Fold Transformation of Logic Programs. In: Proc. 2nd Int. Conf. on Logic Programming, pp. 127–138 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seki, H. (2013). Proving Properties of Co-logic Programs with Negation by Program Transformations. In: Albert, E. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2012. Lecture Notes in Computer Science, vol 7844. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38197-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-38197-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38196-6
Online ISBN: 978-3-642-38197-3
eBook Packages: Computer ScienceComputer Science (R0)