Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-28T04:03:59.276Z Has data issue: false hasContentIssue false
  • English
  • Français

Program completion in the input language of GRINGO*

Published online by Cambridge University Press:  23 August 2017

AMELIA HARRISON ,
VLADIMIR LIFSCHITZ  and
DHANANJAY RAJU
AMELIA HARRISON
Affiliation:
Department of Computer Science, Austin, Texas, USA (e-mails: [email protected], [email protected], [email protected])
VLADIMIR LIFSCHITZ
Affiliation:
Department of Computer Science, Austin, Texas, USA (e-mails: [email protected], [email protected], [email protected])
DHANANJAY RAJU
Affiliation:
Department of Computer Science, Austin, Texas, USA (e-mails: [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We argue that turning a logic program into a set of completed definitions can be sometimes thought of as the “reverse engineering” process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be useful to define completion for a large class of Answer Set Programming (ASP) programs and to automate the process of generating and simplifying completion formulas. Examining the output produced by this kind of software may help programmers to see more clearly what their program does, and to what degree its behavior conforms with their expectations. As a step toward this goal, we propose here a definition of program completion for a large class of programs in the input language of the ASP grounder gringo, and study its properties.

Keywords

formal methodsprogram completionAnswer Set Programming
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 17 , Special Issue 5-6: 33rd International Conference on Logic Programming , September 2017 , pp. 855 - 871
Copyright
Copyright © Cambridge University Press 2017 

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

Footnotes

*

This work was partially supported by the National Science Foundation under Grant IIS-1422455.

References

Clark, K. 1978. Negation as failure. In Logic and Data Bases, Gallaire, H. and Minker, J., Eds. Plenum Press, New York, 293–322.CrossRefGoogle Scholar
Erdem, E. and Lifschitz, V. 2003. Tight logic programs. Theory and Practice of Logic Programming 3, 499–518.CrossRefGoogle Scholar
Fages, F. 1994. Consistency of Clark's completion and 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 Proc. of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 119–131.CrossRefGoogle Scholar
Ferraris, P., Lee, J. and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence 175, 236–263.CrossRefGoogle Scholar
Ferraris, P. and Lifschitz, V. 2010. The stable model semantics for first-order formulas with aggregates. In Proc. of International Workshop on Nonmonotonic Reasoning (NMR) http://www.kr.org/NMR/proceedings.html Google Scholar
Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V. and Schaub, T. 2015. Abstract Gringo. Theory and Practice of Logic Programming 15, 449–463.CrossRefGoogle Scholar
Gurevich, Y. and Shelah, S. 1986. Fixed-point extensions of first-order logic. Annals of Pure and Applied Logic 32, 265–280.CrossRefGoogle Scholar
Harrison, A., Lifschitz, V. and Yang, F. 2014. The semantics of Gringo and infinitary propositional formulas. In Proc. of International Conference on Principles of Knowledge Representation and Reasoning (KR), 32–41.Google Scholar
Lee, J. and Meng, Y. 2009. On reductive semantics of aggregates in answer set programming. In Proc. of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 182–195.CrossRefGoogle Scholar
Lee, J. and Meng, Y. 2012. Stable models of formulas with generalized quantifiers. In Working Notes of the 14th International Workshop on Non-Monotonic Reasoning (NMR).Google Scholar
Truszczynski, M. 2012. Connecting first-order ASP and the logic FO(ID) through reducts. In Correct Reasoning: Essays on Logic-Based AI in Honor of Vladimir Lifschitz, Erdem, E., Lee, J., Lierler, Y. and Pearce, D., Eds. Springer, 543–559.CrossRefGoogle Scholar
Supplementary material: PDF

Harrison et al supplementary material

Online Appendix

Download Harrison et al supplementary material(PDF)
PDF 220.3 KB