9 citations · 18 across the 6 of their papers we have counts for
7 papers
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
José Espírito Santo, Ralph Matthes, Luís Pinto
The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to…
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
José Espírito Santo, Ralph Matthes, Luís Pinto
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting…
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
José Espírito Santo, Ralph Matthes, Luís Pinto
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inferen…
Confluence for classical logic through the distinction between values and computations
José Espírito Santo, Ralph Matthes, Koji Nakazawa +1
We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-e…
A Coinductive Approach to Proof Search
José Espírito Santo, Ralph Matthes, Luís Pinto
We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicationa…
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
Luís Pinto, Tarmo Uustalu
Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem…