Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
| Autor: | Espírito Santo, José, Matthes, Ralph, Pinto, Luís |
|---|---|
| Přispěvatelé: | University of Minho [Braga], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, FCT(Fundação para a Ciência e a Tecnologia) within the Projects UIDB/00013/2020 and UIDP/00013/2020, Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch, European Project: COST Action CA15123 ,COST - European Cooperation in Science and Technology,EUTYPES(2016), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Universidade do Minho, Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Computer Science - Logic in Computer Science
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Ciências Naturais::Ciências da Computação e da Informação Mathematics - Logic 16. Peace & justice Theory of computation → Type theory Inhabitation problems [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Theory of computation → Proof theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Coinduction Lambda-calculus Inhabitation problem [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT] Polarized logic |
| Zdroj: | LIPIcs : 26th International Conference on Types for Proofs and Programs (TYPES 2020) Ugo de'Liguoro; Stefano Berardi; Thorsten Altenkirch. LIPIcs : 26th International Conference on Types for Proofs and Programs (TYPES 2020), 188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany, 2021, LIPIcs : Leibniz International Proceedings in Informatics ; ISSN : 1868-8969, 978-3-95977-182-5. ⟨10.4230/LIPIcs.TYPES.2020.4⟩ |
| DOI: | 10.4230/lipics.types.2020.4 |
| Popis: | The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT. Comment: 22 pages incl. appendices; we now stress the dependence of the results on specific proof systems (seen in the abstract, hence the change of title). LJT now comes at the end of the main text. Thm 8 (was Thm 14) evolved, and we abandon modifications in the vector of declarations in two clauses for finitary representation. There is new material on type finiteness in LJP (developed in the appendix) |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|