Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Strong Equivalence and Program’s Structure in Arguing Essential Equivalence Between First-Order Logic Programs

  • Conference paper
  • First Online:
Practical Aspects of Declarative Languages (PADL 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11372))

Included in the following conference series:

Abstract

Answer set programming is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper claims the correctness of a number of interesting program rewritings. Notably, they assume programs with variables and such important language features as choice, disjunction, and aggregates.

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

Institutional subscriptions

Notes

  1. 1.

    This includes equality statements and the formula \(\bot \).

  2. 2.

    An Herbrand interpretation of a signature \(\sigma \) (containing at least one object constant) is such that its universe is the set of all ground terms of \(\sigma \), and every ground term represents itself. An Herbrand interpretation can be identified with the set of ground atoms (not containing equality) to which it assigns the value true.

References

  1. Ben-Eliyahu, R., Dechter, R.: Propositional semantics for disjunctive logic programs. Ann. Math. Artif. Intell. 12, 53–87 (1994)

    Article  MathSciNet  Google Scholar 

  2. Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Commun. ACM 54(12), 92–103 (2011)

    Article  Google Scholar 

  3. Buddenhagen, M., Lierler, Y.: Performance tuning in answer set programming. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds.) LPNMR 2015. LNCS (LNAI), vol. 9345, pp. 186–198. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23264-5_17

    Chapter  MATH  Google Scholar 

  4. Eiter, T., Fink, M.: Uniform equivalence of logic programs under the stable model semantics. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 224–238. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24599-5_16

    Chapter  MATH  Google Scholar 

  5. Eiter, T., Fink, M., Tompits, H., Traxler, P., Woltran, S.: Replacements in non-ground answer-set programming. In: Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR) (2006)

    Google Scholar 

  6. Eiter, T., Tompits, H., Woltran, S.: On solution correspondences in answer-set programming. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), pp. 97–102 (2005)

    Google Scholar 

  7. Eiter, T., Traxler, P., Woltran, S.: An implementation for recognizing rule replacements in non-ground answer-set programs. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 477–480. Springer, Heidelberg (2006). https://doi.org/10.1007/11853886_41

    Chapter  Google Scholar 

  8. Ferraris, P.: Answer sets for propositional theories. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 119–131. Springer, Heidelberg (2005). https://doi.org/10.1007/11546207_10

    Chapter  Google Scholar 

  9. Ferraris, P., Lee, J., Lifschitz, V.: Stable models and circumscription. Artif. Intell. 175, 236–263 (2011)

    Article  MathSciNet  Google Scholar 

  10. Ferraris, P., Lee, J., Lifschitz, V., Palla, R.: Symmetric splitting in the general theory of stable models. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), pp. 797–803. IJCAI press (2009)

    Google Scholar 

  11. Ferraris, P., Lifschitz, V.: Weight constraints as nested expressions. Theory Pract. Log. Program. 5, 45–74 (2005)

    Article  MathSciNet  Google Scholar 

  12. Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., Schaub, T.: Abstract gringo. Theory Pract. Log. Program. 15, 449–463 (2015). https://doi.org/10.1017/S1471068415000150. http://journals.cambridge.org/article_S1471068415000150

    Article  MathSciNet  Google Scholar 

  13. Gelfond, M., Kahl, Y.: Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach. Cambridge University Press, Cambridge (2014)

    Book  Google Scholar 

  14. Gelfond, M., Lifschitz, V., Przymusińska, H., Truszczyński, M.: Disjunctive defaults. In: Allen, J., Fikes, R., Sandewall, E. (eds.) Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 230–237 (1991)

    Google Scholar 

  15. Harrison, A., Lierler, Y.: First-order modular logic programs and their conservative extensions. In: Theory and Practice of Logic programming, 32nd International Conference on Logic Programming (ICLP) Special Issue (2016)

    Article  MathSciNet  Google Scholar 

  16. Janhunen, T., Oikarinen, E., Tompits, H., Woltran, S.: Modularity aspects of disjunctive stable models. In: Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pp. 175–187 (2007)

    Google Scholar 

  17. Lee, J., Lifschitz, V., Palla, R.: A reductive semantics for counting and choice in answer set programming. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), pp. 472–479 (2008)

    Google Scholar 

  18. Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Trans. Comput. Log. 2, 526–541 (2001)

    Article  MathSciNet  Google Scholar 

  19. Lifschitz, V., Pearce, D., Valverde, A.: A characterization of strong equivalence for logic programs with variables. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483, pp. 188–200. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72200-7_17

    Chapter  MATH  Google Scholar 

  20. Linke, T., Tompits, H., Woltran, S.: On acyclic and head-cycle free nested logic programs. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 225–239. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27775-0_16

    Chapter  MATH  Google Scholar 

  21. Mints, G.: A Short Introduction to Intuitionistic Logic. Springer, New York (2000)

    MATH  Google Scholar 

  22. Pearce, D., Valverde, A.: Synonymous theories and knowledge representations in answer set programming. J. Comput. Syst. Sci. 78(1), 86–104 (2012). https://doi.org/10.1016/j.jcss.2011.02.013. http://www.sciencedirect.com/science/article/pii/S0022000011000420, jCSS Knowledge Representation and Reasoning

    Article  MathSciNet  MATH  Google Scholar 

  23. Woltran, S.: Characterizations for relativized notions of equivalence in answer set programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 161–173. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30227-8_16

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

We are grateful to Vladimir Lifschitz and Miroslaw Truszczynski for valuable discussions on the subject of this paper. Yuliya Lierler was partially supported by the NSF 1707371 grant.

Author information

Authors and Affiliations

  1. University of Nebraska at Omaha, Omaha, USA

    Yuliya Lierler

Authors
  1. Yuliya Lierler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yuliya Lierler .

Editor information

Editors and Affiliations

  1. Universidade Nova de Lisboa, Lisbon, Portugal

    José Júlio Alferes

  2. Chalmers University of Technology, Gothenburg, Sweden

    Moa Johansson

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lierler, Y. (2019). Strong Equivalence and Program’s Structure in Arguing Essential Equivalence Between First-Order Logic Programs. In: Alferes, J., Johansson, M. (eds) Practical Aspects of Declarative Languages. PADL 2019. Lecture Notes in Computer Science(), vol 11372. Springer, Cham. https://doi.org/10.1007/978-3-030-05998-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-05998-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-05997-2

  • Online ISBN: 978-3-030-05998-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation