Skip to main content
SpringerLink
Log in

Generalizing extended execution for normal programs

  • Conference paper
  • First Online:
Logic Program Synthesis and Transformation — Meta-Programming in Logic (META 1994, LOPSTR 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 883))

Abstract

We present a set of inference rules aimed at proving declarative (logical) properties of normal programs. Proofs are goal directed and are performed by means of replacement, simplification and rewriting. This work can be seen as a generalization of Extended Execution [16] which is in turn an extension of the prolog interpreter. We show the soundness of our generalization and discuss its completeness. Two extensive examples are given. We conclude on the relevance of our approach within the general framework of verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. Apt. Introduction to Logic Programming. In J. Van Leeuven, editor, Handbook of Theoretical Computer Science. North Holland, 1990.

    Google Scholar 

  2. A. Bottoni and G.Levi. Computing in the Completion. In Atti dell Ottavo Convegno sulla Programmazione Logica (Gulp), pages 375–389. Mediterranean Press, 1993.

    Google Scholar 

  3. A. Bouverot. Comparaison entre la transformation et l'extraction de programmes logiques. PhD thesis, Université Paris VII, 1991.

    Google Scholar 

  4. P. Bruscoli, F. Levi, G. Levi, and M. C. Meo. Intensional Negation in Constraint Logic Programs. In Atti dell Ottavo Convegno sulla Programmazione Logica (Gulp), pages 359–373. Mediterranean Press, 1993.

    Google Scholar 

  5. K. L. Clark. Negation as Failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293–322. Plenum Press, New York, 1978.

    Google Scholar 

  6. A. Cortesi and G. Filé. Graph Properties for Normal Programs. Theoretical Computer Science, 107:277–303, 1993.

    Google Scholar 

  7. P. Deransart. Proof Methods of Declarative Properties of Definite Programs. Theoretical Computer Science, 118:99–166, 1993.

    Google Scholar 

  8. P. Deransart and G. Ferrand. Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs. Journal of Logic Programming, 17:265–278, 1993.

    Google Scholar 

  9. Y. Deville. A Correctness Definition for Logic Programming. Technical Report RP 88/8, Namur University, 1988.

    Google Scholar 

  10. W. Drabent. What is Failure? An Approach to Constructive Negation. Technical Report LITH-IDA-R-91-23, Linkoping University, 1993. to appear in Acta Informatica.

    Google Scholar 

  11. M. Fitting. A Kripke-Kleene Semantics for Logic Programs. Journal of Logic Programming, 2:295–312, 1985.

    Article  Google Scholar 

  12. L. Fribourg. Extracting Logic Programs from Proofs that Use Extended Prolog Execution and Induction. In Proceedings of the Seventh Int. Conference on Logic Programming, Jerusalem, pages 685–699, 1990.

    Google Scholar 

  13. L. Fribourg. Generating Simplification Lemmas using Extended Prolog Execution and Proof-Extraction. In Proceedings of the Int. Logic Programming Symposium, San Diego, 1991.

    Google Scholar 

  14. A. Van Gelder, K. A. Ross, and J. S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3):620–650, 1991.

    Google Scholar 

  15. T. Kanamori. Soundness and Completeness of Extended Execution for Proving Properties of Prolog Programs. Technical Report TR-175, ICOT, 1986.

    Google Scholar 

  16. T. Kanamori and H. Seki. Verification of Logic Programs Using an Extension of Execution. In Proceedings of the Third International Conference on Logic Programming, London, pages 475–489, 1986.

    Google Scholar 

  17. K. Kunen. Negation in Logic Programming. Journal of Logic Programming, 4:289–308, 1987.

    Article  Google Scholar 

  18. K. Kunen. Signed Data Dependencies in Logic Programs. Journal of Logic Programming, 7:231–245, 1989.

    Article  Google Scholar 

  19. J. L. Lassez, M. J. Maher, and K. G. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Alto, Ca., 1988.

    Google Scholar 

  20. J. M. Lever. Proving Program Properties by means of SLS-resolution. In Proceedings of the Eight Int. Conference on Logic Programming, Paris, pages 614–628, 1991.

    Google Scholar 

  21. J. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987.

    Google Scholar 

  22. T. C. Przymusinski. Perfect Model Semantics. In R. Kowalski and K. Bowen editors, editors, Proceedings of the Fifth Int. Logic Programming Symposium, pages 1081–1096. Association for Logic Programing, 1988.

    Google Scholar 

  23. T. C. Przymusinski. On Constructive Negation in Logic Programming. Technical report, University of Texas at El Paso, 1990.

    Google Scholar 

  24. T. Sato. Equivalence-preserving first order unfold/fold transformation systems. Theoretical Computer Science, 105:57–84, 1992.

    Google Scholar 

  25. T. Sato and F. Motoyoshi. A Complete Top-down Interpreter for First Order Programs. In Proceedings of the Int. Logic Programming Symposium, San Diego, pages 35–53. MIT Press, 1991.

    Google Scholar 

  26. J. C. Shepherdson. Language and Equality Theory in Logic Programming. Technical Report PM-88-08, University of Bristol, 1988.

    Google Scholar 

  27. D. van Dalen. Logic and Structure. Springer Verlag, Berlin, second edition, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA-Rocquencourt, BP 105, 78153, Le Chesnay, France

    Sophie Renault

Authors
  1. Sophie Renault
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Laurent Fribourg Franco Turini

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Renault, S. (1994). Generalizing extended execution for normal programs. In: Fribourg, L., Turini, F. (eds) Logic Program Synthesis and Transformation — Meta-Programming in Logic. META LOPSTR 1994 1994. Lecture Notes in Computer Science, vol 883. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58792-6_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-58792-6_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58792-7

  • Online ISBN: 978-3-540-49104-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation