On Completeness of Logic Programs

  • Włodzimierz DrabentEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)


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.


Logic programming Program completeness Declarative programming Approximate specification 


  1. 1.
    Apt, K.R.: From Logic Programming to Prolog. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1997)Google Scholar
  2. 2.
    Apt, K.R., Pedreschi, D.: Reasoning about termination of pure Prolog programs. Inf. Comput. 106(1), 109–157 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Bezem, M.: Strong termination of logic programs. J. Log. Program. 15(1&2), 79–97 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Clark, K.L.: Predicate logic as computational formalism. Technical report 79/59, Imperial College, London (1979)Google Scholar
  5. 5.
    Deransart, P., Małuszyński, J.: A Grammatical View of Logic Programming. The MIT Press, Cambridge (1993) zbMATHGoogle Scholar
  6. 6.
    Deville, Y.: Logic Programming: Systematic Program Development. Addison-Wesley, Reading (1990)Google Scholar
  7. 7.
    Deville, Y., Lau, K.-K.: Logic program synthesis. J. Log. Program. 19(20), 321–350 (1994)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Doets, K.: From Logic to Logic Programming. The MIT Press, Cambridge (1994)zbMATHGoogle Scholar
  9. 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).
  10. 10.
    Drabent, W.: Logic + control: an example of program construction, CoRR. abs/1110.4978 (2012).
  11. 11.
    Drabent, W.: Correctness and completeness of logic programs, CoRR. abs/1412.8739 (2014).
  12. 12.
    Drabent, W.: On completeness of logic programs, CoRR. abs/1411.3015(2014).
  13. 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)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 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)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Hogger, C.J.: Introduction to Logic Programming. Academic Press, London (1984)zbMATHGoogle Scholar
  16. 16.
    Howe, J.M., King, A.: A pearl on SAT and SMT solving in Prolog. Theor. Comput. Sci. 435, 43–55 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  17. 17.
    King, A.: Personal communication, March 2012Google Scholar
  18. 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. 19.
    Pettorossi, A., Proietti, M.: Transformation of logic programs: foundations and techniques. J. Log. Program. 19/20, 261–320 (1994)CrossRefMathSciNetGoogle Scholar
  20. 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) CrossRefGoogle Scholar
  21. 21.
    Shapiro, E.: Algorithmic Program Debugging. The MIT Press, Cambridge (1983) Google Scholar
  22. 22.
    Stärk, R.F.: The theoretical foundations of LPTP (a logic program theorem prover). J. Log. Program. 36(3), 241–269 (1998)CrossRefzbMATHGoogle Scholar
  23. 23.
    Sterling, L., Shapiro, E.: The Art of Prolog, 2nd edn. The MIT Press, Cambridge (1994) zbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Institute of Computer Science, Polish Academy of Sciences and IDALinköpings UniversitetLinköpingSweden

Personalised recommendations