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.

PDF

Theory and Practice of Logic Programming, Vol. 16, 5-6 (2016), pp. 787--799.

@article{harlifmic:iclp16, title={Proving Infinitary Formulas}, author={Amelia Harrison and Vladimir Lifschitz and Julian Michael}, booktitle={Proceedings of the 32nd International Conference on Logic Programming }, volume={16}, journal={Theory and Practice of Logic Programming}, number={5-6}, pages={787--799}, url="http://www.cs.utexas.edu/users/ai-lab?harlifmic:iclp16", year={2016} }