Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-15T22:18:15.998Z Has data issue: false hasContentIssue false
  • English
  • Français

Proving infinitary formulas

Published online by Cambridge University Press:  14 October 2016

AMELIA HARRISON ,
VLADIMIR LIFSCHITZ  and
JULIAN MICHAEL
AMELIA HARRISON
Affiliation:
University of Texas, Austin, Texas, USA (e-mail: ameliaj@cs.utexas.edu, vl@cs.utexas.edu)
VLADIMIR LIFSCHITZ
Affiliation:
University of Texas, Austin, Texas, USA (e-mail: ameliaj@cs.utexas.edu, vl@cs.utexas.edu)
JULIAN MICHAEL
Affiliation:
University of Washington, Seattle, Washington, USA (e-mail: julianjohnmichael@gmail.com)
Get access Rights & Permissions [Opens in a new window]

Abstract

The infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas.

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 16 , Special Issue 5-6: 32nd International Conference on Logic Programming , September 2016 , pp. 787 - 799
Copyright
Copyright © Cambridge University Press 2016 

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

Clark, K. 1978. Negation as failure. In Logic and Data Bases, Gallaire, H. and Minker, J., Eds. Plenum Press, New York, 293–322.Google Scholar
Eiter, T., Fink, M., Tomits, H. and Woltran, S. 2005. Strong and uniform equivalence in answer-set programming: Characterizations and complexity results for the non-ground case. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 695–700.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.Google Scholar
Harrison, A., Lifschitz, V., Pearce, D. and Valverde, A. 2015. Infinitary equilibrium logic and strong equivalence. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 398–410.Google Scholar
Harrison, A., Lifschitz, V. and Truszczynski, M. 2015. On equivalence of infinitary formulas under the stable model semantics. Theory and Practice of Logic Programming 15, 1, 18–34.CrossRefGoogle Scholar
Hosoi, T. 1966. The axiomatization of the intermediate propositional systems Sn of Gödel. Journal of the Faculty of Science of the University of Tokyo 13, 183–187.Google Scholar
Lifschitz, V., Morgenstern, L. and Plaisted, D. 2008. Knowledge representation and classical logic. In Handbook of Knowledge Representation, van Harmelen, F., Lifschitz, V., and Porter, B., Eds. Elsevier, 3–88.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
Mints, G. 2000. A Short Introduction to Intuitionistic Logic. Kluwer.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
Umezawa, T. 1959. On intermediate many-valued logics. Journal of the Mathematical Society of Japan 11, 2, 116–128.Google Scholar