Proving infinitary formulas. Issue 5 (14th October 2016)

• Record Type: Journal Article
• Authors: HARRISON, AMELIA; LIFSCHITZ, VLADIMIR; MICHAEL, JULIAN
• Editors: Carro, Manuel; King, Andy
• Is Part Of: Theory and practice of logic programming. Volume 16:Issue 5/6(2016)
• Page Start: 787
• Page End: 799
• Publication Date: 2016-10-14
• Subjects: Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068416000302
• Languages: English
• ISSNs: 1471-0684

Abstract

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.