{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,6,22]],"date-time":"2022-06-22T04:29:12Z","timestamp":1655872152794},"reference-count":11,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T00:00:00Z","timestamp":1476403200000},"content-version":"unspecified","delay-in-days":43,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2016,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1017\/s1471068416000302","type":"journal-article","created":{"date-parts":[[2016,10,15]],"date-time":"2016-10-15T17:28:20Z","timestamp":1476552500000},"page":"787-799","source":"Crossref","is-referenced-by-count":1,"title":["Proving infinitary formulas"],"prefix":"10.1017","volume":"16","author":[{"given":"AMELIA","family":"HARRISON","sequence":"first","affiliation":[]},{"given":"VLADIMIR","family":"LIFSCHITZ","sequence":"additional","affiliation":[]},{"given":"JULIAN","family":"MICHAEL","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,10,14]]},"reference":[{"key":"S1471068416000302_ref11","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/01120116"},{"key":"S1471068416000302_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(07)03001-5"},{"key":"S1471068416000302_ref9","volume-title":"A Short Introduction to Intuitionistic Logic","author":"Mints","year":"2000"},{"key":"S1471068416000302_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30743-0_37"},{"key":"S1471068416000302_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068416000302_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000088"},{"key":"S1471068416000302_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000150"},{"key":"S1471068416000302_ref2","unstructured":"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\u2013700."},{"key":"S1471068416000302_ref4","doi-asserted-by":"crossref","unstructured":"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\u2013410.","DOI":"10.1007\/978-3-319-23264-5_33"},{"key":"S1471068416000302_ref8","doi-asserted-by":"crossref","unstructured":"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\u2013200.","DOI":"10.1007\/978-3-540-72200-7_17"},{"key":"S1471068416000302_ref6","first-page":"183","article-title":"The axiomatization of the intermediate propositional systems Sn\n                   of G\u00f6del","volume":"13","author":"Hosoi","year":"1966","journal-title":"Journal of the Faculty of Science of the University of Tokyo"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068416000302","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T20:37:01Z","timestamp":1555619821000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068416000302\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":11,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["S1471068416000302"],"URL":"https:\/\/doi.org\/10.1017\/s1471068416000302","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}