Mathematical Logic Webinar

Coinductive proof search for intuitionistic propositional logic

Transmissão através de Videoconferência

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

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional

Mathematical Logic Webinar, por Luís Pinto (Centro de Matemática - Universidade do Minho).

This course aims to provide students with statistical knowledge and tools to manipulate, analyze and visualize biological data with R. Introduction to modeling, simulations and Bayesian statistics.

LASIGE - driven by excellence

The Workshop aims at reinforcing the connections among its members and the scientific community.

Fotografia de investigador, acompanhada do título do evento

Um dia dedicado à promoção da oferta formativa de mestrados e pós-graduações de Ciências.

Vem desenvolver a tua expressão oral com o auxílio de exercícios teatrais.

Pormenor da Exposição "Formas & Fórmulas" (Ciências, out2016-mar2017)

A sessão tem como objetivo apresentar o programa doutoral, os cursos doutorais abertos em 2021/2022, os temas para tese e seus orientadores.

Logótipo da iniciativa

"Património e divulgação em Paleontologia" é o tema escolhido para esta edição do EJIP.

Geometry Webinar, por Stéphane Guillermou (CNRS, Univ. Grenoble).

Logótipo do ciclo de webinars, sobre um fundo branco

At AppEEL, we aim to advance the study of evolution from an inter- and transdisciplinary approach and to identify how biological evolutionary theories can be applied to the epistemological, sociocultural and linguistic domains.

Capa do livro "O Triunfo dos Jardins"

Lançamento do livro "O Triunfo dos Jardins - O pelouro dos Passeios e Arvoredos de Lisboa (1840-1900)", de Ana Duarte Rodrigues (Ciências ULisboa).

Colóquio de Matemática, por Jorge Buescu (DM-FCUL e CMAFcIO).

Lista de Universidades

Candidaturas até 21 de maio de 2021 (mobilidade no 1.º semestre).

Evento de promoção da investigação na área da Estatística junto dos alunos de Licenciatura e de 1.º ano de Mestrado.

A mostly practical course, offering an overview on different community ecology and macroecological methods and software.

Logótipo da conferência, sobre um fundo branco

THE meeting place for Mobility Management practitioners and experts all over Europe.

An overview of the different ways to measure biodiversity, and provides tips for the stratification of primary biodiversity data and the construction of variables that describe its various facets.

This course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems.

Título e data do evento

An overview of recent developments and applications of the algebraic and analytic theory of D-modules.

How to predict the three-dimensional structure of nucleic acid and proteins from their sequence and use the acquired knowledge to improve or create new methodologies in molecular biology research and diagnostics?

Logótipo do evento, sobre um fundo branco

Welcome to an unique silicon for photovoltaics event in Lisbon!

Logótipo da Unite!

Summer School no âmbito da Rede UNITE! (University Network for Innovation, Technology and Engineering), de que faz parte a ULisboa, com inscrições a decorrer até 15 de maio de 2021.