Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-12-01T00:05:12.087Z Has data issue: false hasContentIssue false
  • English
  • Français

Modular Answer Set Programming as a Formal Specification Language

Published online by Cambridge University Press:  21 September 2020

PEDRO CABALAR Open the ORCID record for PEDRO CABALAR [Opens in a new window] ,
JORGE FANDINNO Open the ORCID record for JORGE FANDINNO [Opens in a new window]  and
YULIYA LIERLER Open the ORCID record for YULIYA LIERLER [Opens in a new window]
PEDRO CABALAR
Affiliation:
University of Corunna, Spain (e-mail: [email protected])
JORGE FANDINNO
Affiliation:
University of Potsdam, Germany (e-mail: [email protected])
YULIYA LIERLER
Affiliation:
University of Nebraska Omaha, USA (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification.

Keywords

Answer Set ProgrammingFormal SpecificationFormal VerificationModular Logic Programs
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 20 , Issue 5: 36th International Conference on Logic Programming Special Issue I , September 2020 , pp. 767 - 782
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aguado, F., Cabalar, P., Fandinno, J., Pearce, D., Pérez, G., and Vidal, C. 2019. Forgetting auxiliary atoms in forks. Artificial Intelligence 275, 575–601.CrossRefGoogle Scholar
Brewka, G., Niemelä, I., and Truszczynski, M. 2011. Answer set programming at a glance. Communications of the ACM 54(12), 92–103.Google Scholar
Buddenhagen, M. and Lierler, Y. 2015. Performance tuning in answer set programming. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR).Google Scholar
Cabalar, P., Fandinno, J., and Lierler, Y. 2020. Modular answer set programming as a formal specification language.CrossRefGoogle Scholar
Denecker, M., Lierler, Y., Truszczyński, M., and Vennekens, J. 2012. A Tarskian informal semantics for answer set programming. In Technical Communications of the 28th International Conference on Logic Programming (ICLP). 277–289.Google Scholar
Eiter, T., Tompits, H., and Woltran, S. 2005. On solution correspondences in answer set programming. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI’05), Kaelbling, L. and Saffiotti, A., Eds. Professional Book Center, 97–102.Google Scholar
Erdoğan, S. T. and Lifschitz, V. 2004. Definitions in answer set programming. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer-Verlag, 114–126.Google Scholar
Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 119–131.Google Scholar
Ferraris, P. 2011. Logic programs with propositional connectives and aggregates. ACM Transactions on Computational Logic 12, 4, 25.Google Scholar
Ferraris, P., Lee, J., and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence 175, 1, 236–263.CrossRefGoogle Scholar
Gebser, M., Kaufmann, B., Neumann, A., and Schaub, T. 2007. Conflict-driven answer set solving. In Proceedings of 20th International Joint Conference on Artificial Intelligence (IJCAI’07). MIT Press, 386–392.Google Scholar
Geibinger, T. and Tompits, H. 2019. Characterising relativised strong equivalence with projection for non-ground answer-set programs. In Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11468. Springer, 542–558.Google Scholar
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the Fifth International Conference and Symposium of Logic Programming (ICLP’88), Kowalski, R. and Bowen, K., Eds. MIT Press, 1070–1080.Google Scholar
Gonçalves, R., Knorr, M., and Leite, J. 2016. You can’t always forget what you want: On the limits of forgetting in answer set programming. In Proceedings of 22nd European Conference on Artificial Intelligence (ECAI’16). Frontiers in Artificial Intelligence and Applications, vol. 285. IOS Press, 957–965.Google Scholar
Harrison, A. and Lierler, Y. 2016. First-order modular logic programs and their conservative extensions. Theory and Practice of Logic programming, 32nd Int’l. Conference on Logic Programming (ICLP) Special Issue.CrossRefGoogle Scholar
Lierler, Y. 2019. Strong equivalence and program’s structure in arguing essential equivalence between first-order logic programs. In Proceedings of the 21st International Symposium on Practical Aspects of Declarative Languages (PADL).Google Scholar
Lifschitz, V. 2017. Achievements in answer set programming. Theory and Practice of Logic Programming 17, 5-6, 961–973.Google Scholar
Lifschitz, V., Lühne, P., and Schaub, T. 2018. anthem: Transforming gringo programs into first-order theories (preliminary report). CoRR abs/1810.00453.Google Scholar
Lifschitz, V., Pearce, D., and Valverde, A. 2001. Strongly equivalent logic programs. ACM Transactions on Computational Logic 2, 4, 526–541.Google Scholar
Lifschitz, V., Pearce, D., and Valverde, A. 2007. A characterization of strong equivalence for logic programs with variables. In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 188–200.Google Scholar
Lifschitz, V. and Turner, H. 1994. Splitting a logic program. In Proceedings of the Eleventh International Conference on Logic Programming. MIT Press, 23–37.Google Scholar
Marek, V. and Truszczyński, M. 1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm: a 25-Year Perspective, Apt, K., Marek, V., Truszczyński, M., and Warren, D., Eds. Springer-Verlag, 375–398.Google Scholar
Monin, J. 2003. Understanding formal methods. Springer.CrossRefGoogle Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 3-4, 241–273.CrossRefGoogle Scholar
Oetsch, J. and Tompits, H. 2008. Program correspondence under the answer-set semantics: The non-ground case. In Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings, de la Banda, M. G. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 591–605.Google Scholar
Oikarinen, E. and Janhunen, T. 2009. A translation-based approach to the verification of modular equivalence. J. Log. Comput. 19, 4, 591–613.Google Scholar
Pearce, D. and Valverde, A. 2004. Synonymous theories in answer set programming and equilibrium logic. In Proceedings of the 16th European Conference on Artificial Intelligence. ECAI’04. IOS Press, Amsterdam, The Netherlands, The Netherlands, 388–392.Google Scholar
Pearce, D. and Valverde, A. 2008. Quantified equilibrium logic and foundations for answer set programs. In Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings, de la Banda, M. G. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 546–560.Google Scholar