Mathematical Logic Seminar

From axioms to synthetic inference rules via focusing

Sala 6.2.33, Ciências ULisboa (com transmissão online)

Por Elaine Pimentel (University College London).

One of the advantages of using sequent systems as a framework for logical reasoning is that the resulting calculi are often simple, have good proof theoretical properties (like cut-elimination, consistency, etc) and can be easily implemented, \eg\ using rewriting.

Hence it would be heaven if we could add axioms in mathematical theories to first order logics and reason about them using all the machinery already built for the sequent framework. Indeed, the general problem of extending standard proof-theoretical results obtained for pure logic to certain classes of non-logical axioms has been the focus of attention for quite some time now.

The main obstacle for this agenda is that adding non-logical axioms to systems while still maintaining the good proof theoretical properties is not an easy task. In fact, adding naively axioms to sequent systems often result in non cut-free systems. One way of circumventing this problem is by treating axioms as theories, added to the sequent context. This is already in Gentzen's consistency proof of elementary arithmetic. Now the derivations have only logical axioms as premises, and cut elimination applies.

But we can do better by transforming axioms into inference rules. In this talk, we will propose a systematic way of adding inference rules to sequent systems. The proposal will be based on the notions of focusing and polarities. We will also discuss how our framework escalates to hypersequents and systems of rules.

This is a joint work with Dale Miller, Sonia Marin and Marco Volpe.


Transmissão via Zoom.

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
“Coroa de Flores” cósmica

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Federica Loiacono (INAF OAS Bologna, Italy).

Seminário de Análise e Equações Diferenciais, por João Pedro Ramos (Instituto Nacional de Matemática Pura e Aplicada).

Logótipo do LIP Summer Internship Program

Um programa destinado a estudantes de Física e Engenharia com interesse em investigação científica e tecnológica, com candidaturas até 15 de maio (nova data).

Título/data/local do evento

No Dia Nacional dos Cientistas, o conhecimento não risca fronteiras.

O Museu Nacional de História Natural e da Ciência da Universidade de Lisboa celebra a Noite Europeia dos Museus (17 de maio) e o Dia Internacional dos Museus (18 de maio). Nestes dias, os Museus abrem as portas e convidam os cidadãos a conhecer os seus acervos, coleções, exposições e atividades.

Seminário do Centro de Física Teórica e Computacional, por João Amaral (Department of Physics and CICECO, University of Aveiro, Portugal).

Bodião-limpador "em ação"

Seminário Doutoral II (Doutoramento em Biologia), por Beatriz Palinhos Pereira.

Seminário de Análise e Equações Diferenciais, por Wladimir Neves (Universidade Federal do Rio de Janeiro).

Título/data/local do evento, logótipos das entidades organizadoras e fotografia de peixe

The event aims to facilitate the exchange of information and knowledge among professionals to advance the understanding, collaboration and capabilities of aquaculture to respond to the impact of climate change in a rapidly changing global environment.

Composição do logótipo da ULisboa e de representação do rosto humano à base de relógios

22 de maio - dois dos doze finalistas da competição são alunos de CIÊNCIAS.

Pintura abstrata azul e rosa

Seminário de Análise e Equações Diferenciais, por Leonid Berlyand (Penn State University).

Technovation Girls Challenge Portugal - Final

Ciências acolhe o evento final do Programa Technovation Girls Challenge Portugal.

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Pier-Stefano Corasaniti (Observatoire de Paris-Meudon, France).

Um programa estruturado que combina discussões em grupo, exploração de carreira e workshops informativos, com inscrições até 23 de maio.

Uma oportunidade para fortalecer a cultura de segurança e bem-estar em CIÊNCIAS.

Logótipo do EVM 2025

Candidaturas até 28 de maio.

Uma oportunidade única para interagir com a comunidade global de computação científica.

Logótipo Moodle

Ação de formação para docentes e investigadores de CIÊNCIAS.

Logótipo Mentimeter

Ação de formação para docentes e investigadores de CIÊNCIAS.

Título/data/local do evento e iconografia representativa de energias renováveis

Inscrições até 16 de maio! Junta-te a esta revolução energética e faz a diferença!

Neste curso ficarás a saber como te podes tornar um permacultor eficiente, produtivo e consciente! O curso está preparado para iniciantes na prática de permacultura.

Formação - Cultivar em Permacultura.

Pessoas a interagirem em frente a um computador portátil

As inscrições para a edição de 2025 da formação decorrem até às 17h do dia 23 de maio.

Curso destinado a estudantes de Mestrado e de Doutoramento, bem como a profissionais que desenvolvam investigação científica na área da saúde.

Químico a escrever fórmulas num quadro

Curso acreditado para efeitos de progressão na carreira dos professores do Ensino Básico e Secundário do Grupo 510 (CCPFC/ACC-118288/22), com candidaturas até 18 de maio.

Páginas