arXiv subjects

Luís Pinto

Publications and source records attributed to Luís Pinto.

7 recordsLinked to original sources

arXiv2025

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

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 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. Inhabitation is taken in a generalized sense, because we also consider when a sequent has a solution, that is a (possibly infinite) run of bottom-up proof search which never fails to apply another inference rule. We provide a very general scheme whose instances are decision problems concerning solutions in LJP having algorithms through the inductive syntax. Polarized logic and LJP can be used as a platform from which proof search for other logics is understood. We illustrate this for the proof systems LJT and LJQ for intuitionistic logic, both equipped with all the connectives. For that we work out respectively a negative and a positive interpretation into LJP, which map formulas of the source logic into formulas in LJP of the said polarity; and this even at the level of the coinductive versions of the three involved proof systems. The interpretations are proved to be, not only faithful, but actually full embeddings, establishing a bijection between the solutions (resp. proofs) of a sequent and the solutions (resp. proofs) of its polarized interpretation. This allows the inheritance to the source systems of the decidability and other results previously obtained for LJP, thereby vastly generalizing the previous results of CoIPS, which were confined to LJT and implicational intuitionistic logic.

cs.LO↗

arXiv2021

A Coinductive Approach to Proof Search through Typed Lambda-Calculi

In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard paradigm of representation, from proofs to solutions: to represent solutions by possibly infinite terms of a dedicated lambda-calculus. This new, comprehensive approach to proof search is exemplified with the sequent calculus LJT for intuitionistic implication logic. A finitary representation is proposed, comprising lambda-terms extended with a formal greatest fixed point, and a type system that can be seen as a logic of coinductive proofs. In the finitary system, fixed-point variables enjoy a relaxed form of binding that allows the detection of cycles through the type system. Formal sums are used to express alternatives in the search process. Moreover, formal sums are used in the coinductive syntax to define "decontraction" (contraction bottom-up) - an operation whose theory we initiate in this paper. As a semantics, we assign a coinductive lambda-term to each finitary term. The main result is the existence of an equivalent finitary representation for any full solution space expressed coinductively. This result is the main ingredient in the proof that our logic of coinductive proofs is sound and complete with respect to the coinductive semantics. These results are the foundation for an original approach to proof search, where the search builds the finitary representation of the full solution space, and the a posteriori analysis typically consisting in applying a syntax-directed procedure or function. The paper illustrates this for proof search and inhabitation problems in the simply-typed lambda-calculus, reviewing results detailed elsewhere, and including new results that obtain extensive generalizations of the so-called monatomic theorem.

cs.LO↗

arXiv2017

Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search

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 representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and the end products are simple, recursive decision procedures and counting functions.

cs.LO↗

arXiv2015

An Elastic Image Registration Approach for Wireless Capsule Endoscope Localization

Wireless Capsule Endoscope (WCE) is an innovative imaging device that permits physicians to examine all the areas of the Gastrointestinal (GI) tract. It is especially important for the small intestine, where traditional invasive endoscopies cannot reach. Although WCE represents an extremely important advance in medical imaging, a major drawback that remains unsolved is the WCE precise location in the human body during its operating time. This is mainly due to the complex physiological environment and the inherent capsule effects during its movement. When an abnormality is detected, in the WCE images, medical doctors do not know precisely where this abnormality is located relative to the intestine and therefore they can not proceed efficiently with the appropriate therapy. The primary objective of the present paper is to give a contribution to WCE localization, using image-based methods. The main focus of this work is on the description of a multiscale elastic image registration approach, its experimental application on WCE videos, and comparison with a multiscale affine registration. The proposed approach includes registrations that capture both rigid-like and non-rigid deformations, due respectively to the rigid-like WCE movement and the elastic deformation of the small intestine originated by the GI peristaltic movement. Under this approach a qualitative information about the WCE speed can be obtained, as well as the WCE location and orientation via projective geometry. The results of the experimental tests with real WCE video frames show the good performance of the proposed approach, when elastic deformations of the small intestine are involved in successive frames, and its superiority with respect to a multiscale affine image registration, which accounts for rigid-like deformations only and discards elastic deformations.

cs.CV↗

arXiv2014

Confluence for classical logic through the distinction between values and computations

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-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's lambda-bar-mu-mu-tilde-calculus without losing confluence, and is based on a distinction of "modes" in the proof expressions and "mode" annotations in types. Modes resemble colors and polarities, but are quite different: we give meaning to them in terms of a monadic meta-language where the distinction between values and computations is fully explored. This meta-language is a refinement of the classical monadic language previously introduced by the authors, and is also developed in the paper.

cs.LO↗

arXiv2013

A Coinductive Approach to Proof Search

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 implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the "solution spaces" (called Böhm forests), which are a representation of all (not necessarily well-founded but still locally well-formed) proofs of a given formula (more generally: of a given sequent). As main result we obtain, for each given formula, the reduction of a coinductive definition of the solution space to a effective coinductive description in a finitary term calculus with a formal greatest fixed-point operator. This reduction works in a quite direct manner for the case of Horn formulas. For the general case, the naive extension would not even be true. We need to study "co-contraction" of contexts (contraction bottom-up) for dealing with the varying contexts needed beyond the Horn fragment, and we point out the appropriate finitary calculus, where fixed-point variables are typed with sequents. Co-contraction enters the interpretation of the formal greatest fixed points - curiously in the semantic interpretation of fixed-point variables and not of the fixed-point operator.

cs.LO↗

arXiv2011

Relating Sequent Calculi for Bi-intuitionistic Propositional Logic

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 of classical logic. In this paper, we compare three sequent calculi for bi-intuitionistic propositional logic: (1) a basic standard-style sequent calculus that restricts the premises of implication-right and exclusion-left inferences to be single-conclusion resp. single-assumption and is incomplete without the cut rule, (2) the calculus with nested sequents by Gore et al., where a complete class of cuts is encapsulated into special "unnest" rules and (3) a cut-free labelled sequent calculus derived from the Kripke semantics of the logic. We show that these calculi can be translated into each other and discuss the ineliminable cuts of the standard-style sequent calculus.

cs.LO↗