Skip to main content

Generalizing allowedness while retaining completeness of SLDNF-resolution

  • Conference paper
  • First Online:

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

Abstract

We propose various generalizations of the usual definition of allowedness used to prove the completeness of SLDNF-resolution. In particular, we define the property of recursively covered programs and goals. We show that, for programs and goals that are call-consistent, even and recursively covered, SLDNF-resolution computes a complete set of ground answers. We then propose further generalized conditions that ensure that SLDNF-resolution is flounder-free. Moreover, this allows us to define a class of programs that subsumes all three major syntactic classes of programs and goals for which SLDNF-resolution is known to be complete; i.e., programs and goals that are either definite, or hierarchical and weakly allowed, or call-consistent, strict and allowed. We conjecture that our generalizations preserve the completeness of SLDNF-resolution. We also investigate the possibility of weakening the other syntactic conditions, i.e., even and call-consistent, while retaining completeness.

supported by ESPRIT BRA 3012

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K.R., Blair, H., Walker, A., Towards a theory of declarative knowledge, in J. Minker (ed), Foundations of Deductive Databases and Logic Programming, Morgan Kaufman, Los Altos, 1988, 89–148.

    Google Scholar 

  2. Barbuti, R., Martelli, M., Completeness of the SLDNF-resolution for a class of logic programs, Proc. 3rd Int. Conf. on Logic Programming, London, 1986, 600–614.

    Google Scholar 

  3. Barbuti, R., Martelli, M., A characterization of non-floundering logic programs and goals based on abstract interpretation techniques, manuscript, Univ. of Pisa, 1988.

    Google Scholar 

  4. Bruynooghe, M., Janssens, G., Callebaut, A., Demoen, B., Abstract interpretation: towards the global optimization of Prolog programs, Proc. 4th Int. Symp. on Logic Programming, San Francisco, 1987, 192–204.

    Google Scholar 

  5. Balbin, I., Port, G.S., Ramamohanarao, K., Magic set computations for stratified databases, TR 87/3, Dept. of Comp. Sc., Univ. Melbourne, Australia, 1987. To appear in J. Logic Programming.

    Google Scholar 

  6. Cavedon, L., On the completeness of SLDNF-resolution, TR 88/17, Dept. of Comp. Sc., Univ. Melbourne, Australia, 1988.

    Google Scholar 

  7. Cavedon, L., Continuity, consistency, and completeness properties for logic programs, Proc. 6th Int. Conf. on Logic Programming, Lisbon, 1989, 571–584.

    Google Scholar 

  8. Cavedon, L., Lloyd, J.W., A completeness theorem for SLDNF resolution, J. Logic Programming 7,3:177–191, 1989.

    Google Scholar 

  9. Cholak, P., Post correspondence problem and Prolog programs, manuscript, Dept. of Mathematics, Univ. Wisconsin, 1988.

    Google Scholar 

  10. Clark, K., Negation as failure, in H. Gallaire, J. Minker (eds), Logic and Data Bases, Plenum Press, New York, 1978, 293–322.

    Google Scholar 

  11. Decker, H., Cavedon, L., Generalizing allowedness while retaining completeness (long version), IR-KB-52, ECRC, 1990.

    Google Scholar 

  12. Dart, P., On derived dependencies and connected databases, manuscript, Dept. of Comp. Sc., Univ. Melbourne, Australia, 1988. To appear in J. Logic Programming.

    Google Scholar 

  13. Decker, H., Domain-independent and range-restricted formulas and deductive databases, Proc. Séminaire sur la Programmation en Logique, CNET, Trégastel, France, 1988, 385–397.

    Google Scholar 

  14. Decker, H., The range form of databases and queries, or: How to avoid floundering, Proc. 5th ÖGAI, Informatik Fachberichte 218, Springer, 1989, 114–123.

    Google Scholar 

  15. Decker, H., Some generalizations of conditions which ensure the completeness of query evaluation, IR-KB-50, ECRC, 1988.

    Google Scholar 

  16. Fitting, M., A Kripke-Kleene semantics for logic programs, J. Logic Programming, 2,4:295–312, 1985.

    Google Scholar 

  17. Jaffar, J., Lassez, J.-L. and Lloyd J.W., Completeness of the negation as failure rule, IJCAI-83, Karlsruhe, 1983, 500–506.

    Google Scholar 

  18. Kunen, K., Negation in logic programming, J. Logic Programming, 4,4:289–308, 1987.

    Article  Google Scholar 

  19. Kunen, K., Signed data dependencies in logic programs, J. Logic Programming 7,3:231–245, 1989.

    Google Scholar 

  20. Kunen, K., Some remarks on the completed database, Proc. 5th Intl. Conf. and Symp. on Logic Programming, 1988, 978–992.

    Google Scholar 

  21. Lloyd, J.W., Foundations of Logic Programming, second edition, Symbolic Computation Series, Springer, 1987 (first edition appeared 1984).

    Google Scholar 

  22. Lloyd, J.W., Shepherdson, J.C., Partial evaluation in logic program, TR-87-09, revised version, Comp. Sc. Dept., Univ. Bristol, 1989.

    Google Scholar 

  23. Lloyd, J.W. and Topor, R.W., Making Prolog more expressive, J. Logic Programming 1,3:225–240, 1984.

    Article  Google Scholar 

  24. Lloyd, J.W. and Topor, R.W., A basis for deductive database systems II, J. Logic Programming 3,1:55–67, 1986.

    Google Scholar 

  25. Mellish, C.S., Abstract interpretation of Prolog programs, Proc. 3rd Int. Conf. on Logic Programming, London, 1986, 463–474.

    Google Scholar 

  26. Przymusinska, H., Przymusinski, T., Semantic issues in deductive databases and logic programs, to appear in A. Banerji (ed), Sourcebook on the Formal Approaches in Artificial Intelligence, North Holland, 1989.

    Google Scholar 

  27. Przymusinski, T., On the declarative and procedural semantics of stratified deductive databases, in J. Minker (ed), Foundations of Deductive Databases and Logic Programming, Morgan Kaufman, Los Altos, 193–216, 1988.

    Google Scholar 

  28. Sato, T., Completed logic programs and their consistency, manuscript, Electrotechnical Lab., Ibaraki, 1988. To appear in J. Logic Programming.

    Google Scholar 

  29. Shepherdson, J.C., Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption, J. Logic Programming, 1,1:51–79, 1984.

    Google Scholar 

  30. Shepherdson, J.C., Negation as failure II, J. Logic Programming, 2,3:185–202, 1985.

    Google Scholar 

  31. Shepherdson, J.C., Negation in logic programming, in J. Minker (ed), Foundations of Deductive Databases and Logic Programming, Morgan Kaufman, Los Altos, 1988, 19–88.

    Google Scholar 

  32. Shepherdson, J.C., A sound and complete semantics for a version of negation as failure, Theoretical Computer Science, 65, 343–371, 1989

    Article  Google Scholar 

  33. Topor, R.W., Domain independent formulas and databases, Theoretical Computer Science, 52,3:281–307, 1987.

    Google Scholar 

  34. J.D. Ullman, Implementation of logical query languages for databases, ACM ToDS 10,3:289–321, 1985.

    Google Scholar 

  35. van Emden, M.H., Kowalski, R., The semantics of predicate logic as a programming language, JACM 23,4:733–742, 1976.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Egon Börger Hans Kleine Büning Michael M. Richter

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Decker, H., Cavedon, L. (1990). Generalizing allowedness while retaining completeness of SLDNF-resolution. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '89. CSL 1989. Lecture Notes in Computer Science, vol 440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52753-2_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-52753-2_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52753-4

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics