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

Seminário de Formação Avançada em Jardins, Paisagens e Ambiente, por Elodie Gomes Marques (DINÂMIA'CET-Iscte - Centro de Estudos sobre a Mudança Socieconomica e o Território).

O programa inclui a atribuição de cartas de reconhecimento de mérito aos melhores alunos que concluíram a licenciatura em Geologia ano letivo 2023, seguida da apresentação do vídeo da excursão final integradora do Mestrado em Geologia da FCUL.

Seminário Doutoral I (Doutoramento em História e Filosofia das Ciências), por Joana Lima de Oliveira.

Logótipo de Ciências ULisboa, título "Dia de Ciências 2024" e frase apelando à participação

23 de abril. Virgínia Dignum, especialista Nações Unidas para IA, é oradora convidada.

Earth Systems Seminar, por Rodrigo Amaro e Silva (IDL, Centre OIE - Mines Paris).

Título/data/local do evento e logótipos das entidades organizadoras

An event specifically focused on technicalities & Data Science.

Logótipo da Marinha, título do programa e indicação dos cursos abrangidos

Sessão de divulgação dirigida aos alunos de Ciências das áreas das Engenharias, Matemática e Química.

Árvore florida

"Em Busca do Transcendente" é o título que o João Fontinha (aluno do Doutoramento em Matemática) escolheu para abrir o programa de primavera.

Talk @LASIGE, por Fernando Gallego Donoso (University of Malaga, Computational Intelligence in Biomedicine - ICB).
 

This 7th edition will once again gather specialists in the field of Combinatorial Optimization from several countries to present and discuss recent research work.

Cromeleque dos Almendres

Sessão no âmbito do ciclo de conversas "Aqui, no Universo", por Fábio Silva e Luís Tirapicos (moderação de Vânia Maia).

Comemorações do 30.º aniversário da VicenTuna - Tuna da Faculdade de Ciências da Universidade de Lisboa.

Título "Bolsas de Doutoramento Unite! ULisboa", logótipos das entidades promotoras e fotografia de jovem investigadora a utilizar um laptop na esplanada de um café

O 3.º concurso decorre até 30 de abril.

Logótipos do programa, de Ciências ULisboa e do GAPsi

Programa de Intervenção de Carreira, com inscrições até 26 de abril.

Fotografia de utente a interagir com um médico através de teleconsulta

O workshop, organizado pela redeSAÚDE da ULisboa, pretende explorar de que forma tecnologias de base digital emergentes na área da saúde podem contribuir para o bem-estar e para a melhoria da prestação de cuidados de saúde.

O encontro reúne cientistas, profissionais e estudantes de diferentes áreas e regiões do país focados em desenvolver a investigação marinha, em linha com a Década da Ciência Oceânica para o Desenvolvimento Sustentável, proclamada pelas Nações Unidas (2021-2030).

Formação modular de 13 de abril a 11 de maio - produção em permacultura.

Logótipo da ação CLEANFOREST

Forests are exposed to multiple global change drivers, wich can constrain their ability to continue providing several ecosystem services (including climate change mitigation). Assessing responses - and underlined mechanisms -  at the whole ecosystem scale is paramount for a holistic understanding of forest response to global change.

Título e data do evento, inseridos em fotografia de cinco jovens em contexto de investigação

Pré-inscrições já disponíveis!

Logótipo do evento

Evento final do Projeto iSEA, com inscrições até 30 de abril.

Título e data do workshop

Workshop no âmbito da recente adesão da Universidade de Lisboa à CoARA - Coalition for Advancing Research Assessment.

Título do curso

Curso Avançado CEAUL / Gades Solutions.

Título e datas de candidatura do programa, sobre um padrão em tons de roxo e laranja

Submissão de candidaturas até 14 de maio.

Os oradores plenários irão falar sobre a importância da interdisciplinaridade de forma acessível para todos, estando previstas palestras e apresentação de pósteres por alunos.

Logótipo do LIP Summer Internship Program e fotografia de jovem investigador

Os estágios podem ter uma duração entre duas semanas e dois meses e realizam-se nos três polos do LIP - candidaturas até 15 de maio.

Páginas