Affordable Access

Proof search for full intuitionistic propositional logic through a coinductive approach for polarized logic

Authors
  • Santo, José Espírito
  • Matthes, Ralph
  • Pinto, Luís
Publication Date
Dec 22, 2020
Source
Hal-Diderot
Keywords
Language
English
License
Unknown
External links

Abstract

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 polarized intuitionistic logic. As before, this includes developing a coinductive description of the search spaces 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. 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 the polarized logic (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.

Report this publication

Statistics

Seen <100 times