Proving Infinitary Formulas (2016)
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.
View:
PDF
Citation:
Theory and Practice of Logic Programming, Vol. 16, 5-6 (2016), pp. 787--799.
Bibtex:

Amelia Harrison Ph.D. Student ameliaj [at] cs utexas edu
Vladimir Lifschitz Faculty vl [at] cs utexas edu
Julian John Michael Undergraduate Alumni julianjm [at] cs utexas edu