Skip to main content
SpringerLink
Log in

Verifleation of Prolog programs using an extension of execution

  • Session 5a: Program Analysis
  • Conference paper
  • First Online:
Book cover Third International Conference on Logic Programming (ICLP 1986)

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

Included in the following conference series:

Abstract

An approach to proving properties of Prolog programs exploiting characteristics of Prolog is described. The most important feature of this approach is the use of an extension of execution, which is a generalization of the conventional Prolog interpreter. We use the extended execution to show that a property S in a class of first order formulas, called S-formulas, is a logical consequence of the completion of a program P. This approach is (1) simple because we need only an extention of the Prolog interpreter, (2) understandable because properties are processed keeping their original forms as far as possible and (3) without waste because we carry it out without unnecessary explicit strengthening of P. We show how the extended execution works for the same example in the Boyer and Moore Theorem Prover (BMTP).

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. Apt, K.R. and M.H. van Emden, “Contribution to the Theory of Logic Programming”, J.ACM, Vol.29, No. 3, pp. 841–862,1982.

    Google Scholar 

  2. Bowen, K.A., “Programming with Full First-Order Logic”, Machine Intelligence 10 (J.E.Hayes, D.Michie and Y-H.Pao Eds), pp.421–440,1982.

    Google Scholar 

  3. Bowen,K.A. and R.A.Kowalski, “Amalgamating Language and Metalanguage in Logic Programming”, in Logic Programming (K.L. Clark and S-Å.Tärnlund Eds), Academic Press, 1980.

    Google Scholar 

  4. Boyer,R.S. and J.S.Moore, “Computational Logic”, Academic Press, 1979.

    Google Scholar 

  5. Clark,K.L. and S-Å.Tärnlund, “A First Order Theory of Data and Programs”, in Information Processing 77 (B.Gilchrist Ed), pp.939–944, 1977.

    Google Scholar 

  6. Clark,K.L., “Negation as Failure”, in Logic and Database (H.Gallaire and J.Minker Eds), pp. 293–302, 1978.

    Google Scholar 

  7. Clark,K.L., “Predicate Logic as a Computational Formalism”, Chap.4, Research Monograph: 79/59, TOC, Imperial College, 1979.

    Google Scholar 

  8. van Emden, M.H. and R.A. Kowalski, “The Semantics of Predicate Logic as a Programing Language”, J. ACM, Vol. 23, No. 4, pp. 733–742, 1976.

    Google Scholar 

  9. Hansson,A. and S-Å.Tärnlund, “A Natural Programming Calculus”, Proc.6th International Joint Conference on Artificial Intelligence, pp.348–355, 1979.

    Google Scholar 

  10. Haridi,S. and D.Sahlin, “Evaluation of Logic Programs Based on Natural Deduction”, Proc. 2nd Workshop on Logic Programming, 1983.

    Google Scholar 

  11. Jaffar, J.,J-L. Lassez and J. Lloyd, “Completeness of the Negation as Failure Rule”, Proc. IJCAI83, Vol.1, pp.500–506, 1983.

    Google Scholar 

  12. Kanamori,T. and H.Fujita, “Formulation of Induction Formulas in Verification of Prolog Programs”, ICOT Technical Report, TR-094, 1984.

    Google Scholar 

  13. Kanamori, T. and K.Horiuchi, “Type Inference in Prolog and Its Applications”, ICOT Technical Report, TR-095, 1984.

    Google Scholar 

  14. Kowalski,R.A., “Logic for Problem Solving”, Chap. 10–12, North Holland, 1980.

    Google Scholar 

  15. Manna, Z. and R. Waldinger, “A Deductive Approach to Program Synthesis”, ACM TOPLAS, Vol. 2, No. 1, pp. 90–121,1980.

    Google Scholar 

  16. Murray, N.V., “Completely Non-Clausal Theorem Proving”, Artificial Intelligence, Vol. 18, pp. 67–85, 1982.

    Article  Google Scholar 

  17. Pereira, L.M.,F.C.N. Pereira and D.H.D. Warren, “User's Guide to DECsystem-10 Prolog”, Occasional Paper 15, Dept. of Artificial Intelligence, Edinburgh, 1979.

    Google Scholar 

  18. Prawitz, D., “Natural Deduction,A Proof Theoretical Study”, Almqvist & Wiksell, Stockholm, 1965.

    Google Scholar 

  19. Schütte,K., “Proof Theory”, (translated by J.N.Crossley), Springer Verlag, 1977.

    Google Scholar 

  20. Stering, L. and A. Bundy, “Meta-Level Inference and Program Verification”, in 6th Automated Deduction (W.Bibel Ed), Lecture Notes in Computer Science 138, pp. 144–150, 1982.

    Google Scholar 

  21. Tamaki,H. and T.Sato, “Unfold/Fold Transformation of Logic Programs”, Proc. 2nd International Logic Programming Conference, pp. 127–138, 1984.

    Google Scholar 

  22. Tärnlund,S.-Å., “Logic Programming Language Based on A Natural Deduction System”, UPMAIL Technical Report, No. 6, 1981.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Central Research Laboratory, Mitsubishi Electric Corporation, Tsukaguchi-Honmachi 8-1-1, 661, Amagasaki, Hyogo, Japan

    Tadashi Kanamori

  2. ICOT Research Center Institute for New Generation Computer Technology, Mita 1-4-28,Minato-ku, 108, Tokyo, Japan

    Hirohisa Seki

Authors
  1. Tadashi Kanamori
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hirohisa Seki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ehud Shapiro

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kanamori, T., Seki, H. (1986). Verifleation of Prolog programs using an extension of execution. In: Shapiro, E. (eds) Third International Conference on Logic Programming. ICLP 1986. Lecture Notes in Computer Science, vol 225. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16492-8_96

Download citation

  • DOI: https://doi.org/10.1007/3-540-16492-8_96

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16492-0

  • Online ISBN: 978-3-540-39831-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation