Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-17T18:22:18.486Z Has data issue: false hasContentIssue false
  • English
  • Français

Verifying Tight Logic Programs with anthem and vampire

Published online by Cambridge University Press:  21 September 2020

JORGE FANDINNO Open the ORCID record for JORGE FANDINNO [Opens in a new window] ,
VLADIMIR LIFSCHITZ Open the ORCID record for VLADIMIR LIFSCHITZ [Opens in a new window] ,
PATRICK LÜHNE Open the ORCID record for PATRICK LÜHNE [Opens in a new window]  and
TORSTEN SCHAUB Open the ORCID record for TORSTEN SCHAUB [Opens in a new window]
JORGE FANDINNO
Affiliation:
University of Potsdam, Germany
VLADIMIR LIFSCHITZ
Affiliation:
University of Texas at Austin, USA
PATRICK LÜHNE
Affiliation:
University of Potsdam, Germany
TORSTEN SCHAUB
Affiliation:
University of Potsdam, Germany
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.

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. 735 - 750
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

Brewka, G., Eiter, T., and Truszczyński, M. 2011. Answer set programming at a glance. Communications of the ACM 54, 12, 92–103.Google Scholar
Cabalar, P., Fandinno, J., and Lierler, Y. 2020. Modular answer set programming as a formal specification language. Theory and Practice of Logic Programming, this volume.Google Scholar
Clark, K. 1978. Negation as failure. In Logic and Data Bases, Plenum Press, 293–322.Google Scholar
Erdem, E. and Lifschitz, V. 2003. Tight logic programs. Theory and Practice of Logic Programming 3, 4-5, 499–518.CrossRefGoogle Scholar
Fages, F. 1994. Consistency of Clark’s completion and the existence of stable models. Journal of Methods of Logic in Computer Science 1, 51–60.Google Scholar
Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning, Springer, 119–131.Google Scholar
Ferraris, P., Lee, J., and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence 175, 1, 236–263.Google Scholar
Ferraris, P., Lee, J., Lifschitz, V., and Palla, R. 2009. Symmetric splitting in the general theory of stable models. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, AAAI/MIT Press, 797–803.Google Scholar
Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., and Schaub, T. 2015. Abstract Gringo. Theory and Practice of Logic Programming 15, 4-5, 449–463.Google Scholar
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the 5th International Conference on Logic Programming, MIT Press, 1070–1080.Google Scholar
Gelfond, M. and Przymusinska, H. 1996. Towards a theory of elaboration tolerance: Logic programming approach. International Journal of Software Engineering and Knowledge Engineering 6, 1, 89–112.Google Scholar
Harrison, A., Lifschitz, V., Pearce, D., and Valverde, A. 2017. Infinitary equilibrium logic and strongly equivalent logic programs. Artificial Intelligence 246, 22–33.Google Scholar
Harrison, A., Lifschitz, V., and Raju, D. 2017. Program completion in the input language of GRINGO. Theory and Practice of Logic Programming 17, 5-6, 855–871.CrossRefGoogle Scholar
Kovács, L. and Voronkov, A. 2013. First-order theorem proving and Vampire. In Proceedings of the 25th International Conference on Computer Aided Verification, Springer, 1–35.Google Scholar
Lee, J., Lifschitz, V., and Palla, R. 2008. A reductive semantics for counting and choice in answer set programming. In Proceedings of the 23rd National Conference on Artificial Intelligence, AAAI Press, 472–479.Google Scholar
Lifschitz, V., Lühne, P., and Schaub, T. 2018. anthem: Transforming gringo programs into first-order theories (preliminary report). In Proceedings of the 11th Workshop on Answer Set Programming and Other Computing Paradigms,Google Scholar
Lifschitz, V., Lühne, P., and Schaub, T. 2019. Verifying strong equivalence of programs in the input language of GRINGO. In Proceedings of the 15th International Conference and Symposium of Logic Programming and Nonmonotonic Reasoning, Springer, 270–283.Google Scholar
Lifschitz, V., Lühne, P., and Schaub, T. 2020. Towards verifying logic programs in the input language of CLINGO. In Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday, Springer, 190–209.Google Scholar
Oikarinen, E. and Janhunen, T. 2009. A translation-based approach to the verification of modular equivalence. Journal of Logic and Computation 19, 4, 591–613.Google Scholar
Sutcliffe, G. 2017. The TPTP problem library and associated infrastructure. Journal of Automated Reasoning 59, 4, 483–502.Google Scholar
Truszczyński, M. 2012. Connecting first-order ASP and the logic FO(ID) through reducts. In Correct Reasoning: Essays on Logic-Based AI in Honour of Vladimir Lifschitz, Springer, 543–559.Google Scholar
Supplementary material: PDF

Fandinno et al. supplementary material

Fandinno et al. supplementary material 1

Download Fandinno et al. supplementary material(PDF)
PDF 324.7 KB
Supplementary material: File

Fandinno et al. supplementary material

Fandinno et al. supplementary material 2

Download Fandinno et al. supplementary material(File)
File 294.8 KB