Skip to main content
SpringerLink
Log in

Acceptability with General Orderings

  • Chapter
  • First Online:
Computational Logic: Logic Programming and Beyond

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2407))

Abstract

We present a new approach to termination analysis of logic programs. The essence of the approach is that we make use of general orderings (instead of level mappings), like it is done in transformational approaches to logic program termination analysis, but we apply these orderings directly to the logic program and not to the term-rewrite system obtained through some transformation. We define some variants of acceptability, based on general orderings, and show how they are equivalent to LD-termination. We develop a demand driven, constraint-based approach to verify these acceptability-variants.

The advantage of the approach over standard acceptability is that in some cases, where complex level mappings are needed, fairly simple orderings may be easily generated. The advantage over transformational approaches is that it avoids the transformation step all together.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Aguzzi and U. Modigliani. Proving Termination of Logic Program by Transforming them into Equivalent Term Rewriting Systems. In Proc. of 13th Conference on Foundations of Software Technologies and Theoretical Computer Science (FST& TCS), pages 114–124. Springer Verlag, 1993. LNCS 761.

    Google Scholar 

  2. K. R. Apt. From Logic Programming to Prolog. Prentice-Hall Int. Series in Computer Science. Prentice Hall, 1997.

    Google Scholar 

  3. K. R. Apt and S. Etalle. On the unification free Prolog programs. In A. M. Borzyszkowski and S. Sokolowski, editors, 18th Int. Symp. on Mathematical Foundations of Computer Science, pages 1–19. Springer Verlag, 1993. LNCS 711.

    Google Scholar 

  4. K. R. Apt and D. Pedreschi. Studies in Pure Prolog: Termination. In J. W. Lloyd, editor, Proc. Esprit Symp. on Logic, pages 150–176. Springer Verlag, 1990.

    Google Scholar 

  5. T. Arts. Automatically proving termination and innermost normalisation of term rewriting systems. PhD thesis, Universiteit Utrecht, 1997.

    Google Scholar 

  6. T. Arts and H. Zantema. Termination of logic programs using semantic unification. In M. Proietti, editor, 5th Int. Workshop on Logic Programming Synthesis and Transformation, pages 219–233. Springer Verlag, 1995. LNCS 1048.

    Google Scholar 

  7. A. Bossi and N. Cocco. Preserving universal temination through unfold/fold. In G. Levi and M. Rodríguez-Artalejo, editors, Algebraic and Logic Programming, pages 269–286. Springer Verlag, 1994. LNCS 850.

    Google Scholar 

  8. A. Bossi, N. Cocco, and M. Fabris. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science, 124(2): 297–328, February 1994.

    Google Scholar 

  9. F. Bueno, M. J. García de la Banda, and M. V. Hermenegildo. Effectiveness of global analysis in strict independence-based automatic parallelization. In M. Bruynooghe, editor, Logic Programming, Proc. of the 1994 Int. Symp., pages 320–336. MIT Press, 1994.

    Google Scholar 

  10. D. De Schreye and S. Decorte. Termination of logic programs: The never-ending story. J. Logic Programming, 19/20:199–260, May/July 1994.

    Google Scholar 

  11. D. De Schreye, K. Verschaetse, and M. Bruynooghe. A framework for analyzing the termination of definite logic programs with respect to call patterns. In I. Staff, editor, Proc. of the Int. Conf. on Fifth Generation Computer Systems., pages 481–488. IOS Press, 1992.

    Google Scholar 

  12. S. Decorte and D. De Schreye. Termination analysis: some practical properties of the norm and level mapping space. In J. Jaffar, editor, Proc. of the 1998 Joint Int. Conf. and Symp. on Logic Programming, pages 235–249. MIT Press, June 1998.

    Google Scholar 

  13. S. Decorte, D. De Schreye, and H. Vandecasteele. Constraint-based termination analysis of logic programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 21(6):1137–1195, November 1999.

    Google Scholar 

  14. N. Dershowitz. Termination. In C. Kirchner, editor, First Int. Conf. on Rewriting Techniques and Applications, pages 180–224. Springer Verlag, 1985. LNCS 202.

    Google Scholar 

  15. N. Dershowitz and C. Hoot. Topics in termination. In C. Kirchner, editor, Rewriting Techniques and Applications, 5th Int. Conf., pages 198–212. Springer Verlag, 1993. LNCS 690.

    Google Scholar 

  16. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM (CACM), 22(8):465–476, August 1979.

    Google Scholar 

  17. S. Etalle, A. Bossi, and N. Cocco. Termination of well-moded programs. J. Logic Programming, 38(2):243–257, February 1999.

    Google Scholar 

  18. H. Ganzinger and U. Waldmann. Termination proofs of well-moded logic programs via conditional rewrite systems. In M. Rusinowitch and J.-L. Remy, editors, Proc. of CTRS’92, pages 216–222. Springer Verlag, 1993. LNCS 656.

    Google Scholar 

  19. S. Hoarau. Inférer et compiler la terminaison des programmes logiques avec contraintes. PhD thesis, Université de La Réunion, 1999.

    Google Scholar 

  20. J. Hsiang. Rewrite method for theorem proving in first order theory with equality. Journal of Symbolic Computation, 8:133–151, 1987.

    Article  MathSciNet  Google Scholar 

  21. G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. J. Logic Programming, 13(2&3):205–258, July 1992.

    Google Scholar 

  22. M. Krishna Rao, D. Kapur, and R. Shyamasundar. Transformational methodology for proving termination of logic programs. J. Logic Programming, 34:1–41, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  23. N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs. In L. Naish, editor, Proc. of the Fourteenth Int. Conf. on Logic Programming, pages 63–77. MIT Press, July 1997.

    Google Scholar 

  24. M. Marchiori. Logic programs as term rewriting systems. In Proc. of the Algebraic Logic Programming ALP’94, pages 223–241. Springer Verlag, 1994. LNCS; volume 850.

    Google Scholar 

  25. L. Plümer. Termination Proofs for Logic Programs. LNAI 446. Springer Verlag, 1990.

    Google Scholar 

  26. S. Ruggieri. Verification and validation of logic programs. PhD thesis, Universitá di Pisa, 1999.

    Google Scholar 

  27. A. Serebrenik and D. De Schreye. Termination analysis of logic programs using acceptability with general term orders. Technical Report CW 291, Departement Computerwetenschappen, K.U.Leuven, Leuven, Belgium, 2000. Available at http://www.cs.kuleuven.ac.be/publicaties/rapporten/CW2000.html.

    Google Scholar 

  28. J.-G. Smaus. Modes and Types in Logic Programming. PhD thesis, University of Kent, 1999.

    Google Scholar 

  29. L. Sterling and E. Shapiro. The Art of Prolog. The MIT Press, 1994.

    Google Scholar 

  30. C. Taboch. A semantic basis for termination analysis of logic programs. Master’s thesis, Ben-Gurion University of the Negev, 1998.

    Google Scholar 

  31. J. D. Ullman and A. van Gelder. Efficient tests for top-down termination of logical rules. Journal of the Association for Computing Machinery, 35(2):345–373, April 1988.

    Google Scholar 

  32. S. Verbaeten. Static verification of compositionality and termination for logic programming languages. PhD thesis, Department of Computer Science, K.U.Leuven, Leuven, Belgium, June 2000. v+265+xxvii.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, K.U. Leuven, Celestijnenlaan 200A, B-3001, Heverlee, Belgium

    Danny De Schreye & Alexander Serebrenik

Authors
  1. Danny De Schreye
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Serebrenik
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Cyprus, 75 Kallipoleos St., 1678, Nicosia, Cyprus

    Antonis C. Kakas

  2. Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen’s Gate, London, SW7 2BZ, UK

    Fariba Sadri

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

De Schreye, D., Serebrenik, A. (2002). Acceptability with General Orderings. In: Kakas, A.C., Sadri, F. (eds) Computational Logic: Logic Programming and Beyond. Lecture Notes in Computer Science(), vol 2407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45628-7_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-45628-7_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43959-2

  • Online ISBN: 978-3-540-45628-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation