Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Logic-Based Program Synthesis and Transformation

LOPSTR 2014: Logic-Based Program Synthesis and Transformation pp 261–278Cite as

On Completeness of Logic Programs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8981))

Abstract

Program correctness (in imperative and functional programming) splits in logic programming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. Little work has been devoted to reasoning about completeness. This paper presents a few sufficient conditions for completeness of definite programs. We also study preserving completeness under some cases of pruning of SLD-trees (e.g. due to using the cut).

We treat logic programming as a declarative paradigm, abstracting from any operational semantics as far as possible. We argue that the proposed methods are simple enough to be applied, possibly at an informal level, in practical Prolog programming. We point out importance of approximate specifications.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    The same holds for \(A\) of the form \(q(s_{11}\mathtt{-}s_{11},s_2)\), or \(q(s_{11}\mathtt{-}s_{12},s_2)\) with non-unifiable \(s_{11}\), \(s_{12}\). The pruning is implemented using the if-then-else construct in Prolog: \(\mathtt{q(V-P,[A|T]) :\!\!-\,V=\,P\, -\!\!\!> true;\, p(A,T).}\) (And the first case of pruning by \(\mathtt{p(V-P,[B|T]):\!\!-\, non{}var(V)\,-\!\!\!> q(V-P,[B|T]);}\,\, \mathtt{q(B,[V-P|T])}.)\)

  2. 2.

    In [9] a weaker version of Theorem 18 was used, and one case of pruning was discussed informally. A proof covering both cases of pruning is illustrated here in Example 20.

References

  1. Apt, K.R.: From Logic Programming to Prolog. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1997)

    Google Scholar 

  2. Apt, K.R., Pedreschi, D.: Reasoning about termination of pure Prolog programs. Inf. Comput. 106(1), 109–157 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bezem, M.: Strong termination of logic programs. J. Log. Program. 15(1&2), 79–97 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  4. Clark, K.L.: Predicate logic as computational formalism. Technical report 79/59, Imperial College, London (1979)

    Google Scholar 

  5. Deransart, P., Małuszyński, J.: A Grammatical View of Logic Programming. The MIT Press, Cambridge (1993)

    MATH  Google Scholar 

  6. Deville, Y.: Logic Programming: Systematic Program Development. Addison-Wesley, Reading (1990)

    Google Scholar 

  7. Deville, Y., Lau, K.-K.: Logic program synthesis. J. Log. Program. 19(20), 321–350 (1994)

    Article  MathSciNet  Google Scholar 

  8. Doets, K.: From Logic to Logic Programming. The MIT Press, Cambridge (1994)

    MATH  Google Scholar 

  9. Drabent, W.: Logic + control: an example. In: Dovier, A., Santos Costa, V. (eds.) Technical Communications of ICLP 2012. LIPIcs, vol. 17, pp. 301–311 (2012). http://drops.dagstuhl.de/opus/volltexte/2012/3631

  10. Drabent, W.: Logic + control: an example of program construction, CoRR. abs/1110.4978 (2012). http://arxiv.org/abs/1110.4978.

  11. Drabent, W.: Correctness and completeness of logic programs, CoRR. abs/1412.8739 (2014). http://arxiv.org/abs/1412.8739

  12. Drabent, W.: On completeness of logic programs, CoRR. abs/1411.3015(2014). http://arxiv.org/abs/1411.3015

  13. Drabent, W., Miłkowska, M.: Proving correctness and completeness of normal programs - a declarative approach. Theory Pract. Log. Program. 5(6), 669–711 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  14. Genaim, S., King, A.: Inferring non-suspension conditions for logic programs with dynamic scheduling. ACM Trans. Comput. Log. 9(3), 17:1–17:43 (2008)

    Article  MathSciNet  Google Scholar 

  15. Hogger, C.J.: Introduction to Logic Programming. Academic Press, London (1984)

    MATH  Google Scholar 

  16. Howe, J.M., King, A.: A pearl on SAT and SMT solving in Prolog. Theor. Comput. Sci. 435, 43–55 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  17. King, A.: Personal communication, March 2012

    Google Scholar 

  18. Kowalski, R.A.: The relation between logic programming and logic specification. In: Hoare, C., Shepherdson, J. (eds.) Mathematical Logic and Programming Languages, pp. 11–27. Prentice-Hall, Upper Saddle River (1985). Also in Phil. Trans. R. Soc. Lond. A, 312, 345–361(1984)

    Google Scholar 

  19. Pettorossi, A., Proietti, M.: Transformation of logic programs: foundations and techniques. J. Log. Program. 19/20, 261–320 (1994)

    Article  MathSciNet  Google Scholar 

  20. Pettorossi, A., Proietti, M., Senni, V.: The transformational approach to program development. In: Dovier, A., Pontelli, E. (eds.) GULP. LNCS, vol. 6125, pp. 112–135. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Shapiro, E.: Algorithmic Program Debugging. The MIT Press, Cambridge (1983)

    Google Scholar 

  22. Stärk, R.F.: The theoretical foundations of LPTP (a logic program theorem prover). J. Log. Program. 36(3), 241–269 (1998)

    Article  MATH  Google Scholar 

  23. Sterling, L., Shapiro, E.: The Art of Prolog, 2nd edn. The MIT Press, Cambridge (1994)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Polish Academy of Sciences and IDA, Linköpings Universitet, Linköping, Sweden

    Włodzimierz Drabent

Authors
  1. Włodzimierz Drabent
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Włodzimierz Drabent .

Editor information

Editors and Affiliations

  1. IASI-CNR, Rome, Italy

    Maurizio Proietti

  2. Nagoya Institute of Technology, Nagoya, Japan

    Hirohisa Seki

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Drabent, W. (2015). On Completeness of Logic Programs. In: Proietti, M., Seki, H. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2014. Lecture Notes in Computer Science(), vol 8981. Springer, Cham. https://doi.org/10.1007/978-3-319-17822-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-17822-6_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-17821-9

  • Online ISBN: 978-3-319-17822-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation