Skip to main content

Equivalence in Answer Set Programming

  • Conference paper
  • First Online:
Logic Based Program Synthesis and Transformation (LOPSTR 2001)

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

Abstract

We study the notion of strong equivalence between two Answer Set programs and we show how some particular cases of testing strong equivalence between programs can be reduced to verify if a formula is a theorem in intuitionistic or classical logic. We present some program transformations for disjunctive programs, which can be used to simplify the structure of programs and reduce their size. These transformations are shown to be of interest for both computational and theoretical reasons. Then we propose how to generalize such transformations to deal with free programs (which allow the use of default negation in the head of clauses). We also present a linear time transformation that can reduce an augmented logic program (which allows nested expressions in both the head and body of clauses) to a program consisting only of standard disjunctive clauses and constraints.

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

Access this chapter

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Arrazola, J. Dix and M. Osorio. Confluent term rewriting systems for nonmonotonic reasoning. Computación y Sistemas, II(2–-3):299–324, 1999.

    Google Scholar 

  2. Y. Babovich, E. Erdem, and V. Lifschitz. Fages’ theorem and answer set programming. In Proceedings of the 8th International Workshop on Non-Monotonic Reasoning, 2000.

    Google Scholar 

  3. C. Baral and M. Gelfond. Reasoning agents in dynamic domain. In J. Minker, editor, Logic Based Artificial Intelligence, pages 257–279. Kluwer, 2000.

    Google Scholar 

  4. S. Brass and J. Dix. Characterizations of the Disjunctive Stable Semantics by Partial Evaluation. Journal of Logic Programming, 32(3):207–228, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  5. S. Brass and J. Dix. Characterizations of the Disjunctive Well-founded Semantics: Confluent Calculi and Iterated GCWA. Journal of Automated Reasoning, 20(1):143–165, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  6. S. Brass, J. Dix, B. Freitag and U. Zukowski. Transformation-based bottom-up computation of the well-founded model. Theory and Practice of Logic Programming, 1(5):497–538, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  7. Y. Dimopoulos, B. Nebel and J. Koehler. Encoding planning problems in nonmonotonic logic programs. In Proceedings of the Fourth European Conference on Planning, pages 169–181. Springer-Verlag, 1997.

    Google Scholar 

  8. J. Dix. A Classification-Theory of Semantics of Normal Logic Programs: II. Weak Properties. Fundamenta Informaticae, XXII(3):257–288, 1995.

    MathSciNet  Google Scholar 

  9. J. Dix, J. Arrazola and M. Osorio. Confluent rewriting systems in non-monotonic reasoning. Computación y Sistemas, Volume II, No. 2–3:104–123, 1999.

    Google Scholar 

  10. J. Dix, M. Osorio and C. Zepeda. A General Theory of Confluent Rewriting Systems for Logic Programming and its Applications. Annals of Pure and Applied Logic, Volume 108, pages 153–188, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  11. M. Gelfond, M. Balduccini and J. Galloway. Diagnosing Physical Systems in A-Prolog. In T. Eiter, W. Faber and M. Truszczynski, editors, Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, pages 213–226, Vienna, Austria, 2001.

    Google Scholar 

  12. M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In R. Kowalski and K. Bowen, editors, 5th Conference on Logic Programming, pages 1070–1080. MIT Press, 1988.

    Google Scholar 

  13. D. Jongh and A. Hendriks. Characterization of strongly equivalent logic programs in intermediate logics. http://turing.wins.uva.nl/lhendrik/ , 2001.

  14. V. Lifschitz. Foundations of logic programming. In Principles of Knowledge Representation, pages 69–127. CSLI Publications, 1996.

    Google Scholar 

  15. V. Lifschitz, D. Pearce and A. Valverde. Strongly equivalent logic programs. ACM Transactions on Computational Logic, 2:526–541, 2001.

    Article  MathSciNet  Google Scholar 

  16. J. Lloyd. Foundations of Logic Programming. Springer, Berlin, 1987. 2nd edition.

    Google Scholar 

  17. M. Osorio, J. Nieves and C. Giannella. Useful transformation in answer set programming. In A. Provetti and T. Son, editors, Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, pages 146–152. AAAI Press, Stanford, USA, 2001.

    Google Scholar 

  18. M. Osorio and F. Zacarias. High-level logic programming. In B. Thalheim and K.-D. Schewe, editors, FolKS, LNCS 1762, pages 226–240. Springer Verlag, Berlin, 2000.

    Google Scholar 

  19. A. Pettorossi and M. Proietti. Transformation of Logic Programs. In D. Gabbay, C. Hogger and J. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 5, pages 697–787. Oxford University Press, 1998.

    Google Scholar 

  20. C. Sakama and K. Inoue. Negation as Failure in the Head. Journal of Logic Programming, 35(1):39–78, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  21. P. Simons. Towards constraint satisfaction through logic programs and the stable model semantics. Technical Report 47, Helsinki University of Technology, Digital Systems Laboratory, August 1997.

    Google Scholar 

  22. L. Tang, V. Lifschitz and H. Turner. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25:369–389, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  23. P. Taylor, J. Girard and Y. Lafont. Proofs and types. Cambridge University Press, 1989.

    Google Scholar 

  24. H. Zhang. Sato: A decision procedure for propositional logic. Association for Automated Reasoning Newsletter, 22:1–3, March 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Osorio, M., Navarro, J.A., Arrazola, J. (2002). Equivalence in Answer Set Programming. In: Pettorossi, A. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2001. Lecture Notes in Computer Science, vol 2372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45607-4_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-45607-4_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43915-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics