Por Luís Pinto (Centro de Matemática - Universidade do Minho).
The coinductive approach to proof search we present is based on three main ideas: (i) the Curry-Howard paradigm of representation of proofs (by typed lambda-terms) is extended to solutions of proof-search problems (a solution is a run of the proof search process that does not fail to apply bottom-up an inference rule, so it may be an infinite object); (ii) two typed lambda-calculi, one obtained by a coinductive reading of the grammar of proof terms (acting as the universe for the mathematical definition of proof search concepts), the other by enriching the grammar of proof terms with a formal fixed-point operator to represent cyclic behaviour (acting as the finitary setting where algorithmic counterparts of those concepts can be found); (iii) formal (finite) sums are employed throughout to represent choice points, so not only solutions but even entire solution spaces are represented, both coinductively and finitarily.
In this seminar we will illustrate this approach for intuitionistic implication, including applications to inhabitation and counting problems in simply-typed lambda-calculus (e. g., results ensuring uniqueness of inhabitants related to coherence in category theory), and briefly overview recent developments on the extension of the approach to polarized intuitionistic logic, which allows to obtain results about proof search for full intuitionistic propositional logic.
This seminar is based on joint work with José Espírito Santo (CMAT, Univ. Minho) and Ralph Matthes (IRIT, CNRS and Univ. Toulouse III, France).
Zoom | ID da reunião: 890 8479 3299 - senha de acesso: 409604
