Mathematical Logic Seminar

A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems

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

Por Carlos Olarte (LIPN, Université Sorbonne Paris Nord).

We develop an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-admissibility, and identity expansion. Although undecidable in general, these properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms, together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies, the L-Framework achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics.

Joint work with Elaine Pimentel and Camilo Rocha.


Transmissão via Zoom.

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Logótipos Ciências ULisboa e C-Academy, títulos dos cursos

Um programa de formação avançada em Cibersegurança para a administração pública e o setor privado desenvolvido pelo Centro Nacional de Cibersegurança, no âmbito do Plano de Recuperação e Resiliência.

Logótipos Ciências ULisboa e C-Academy, títulos dos cursos

Um programa de formação avançada em Cibersegurança para a administração pública e o setor privado desenvolvido pelo Centro Nacional de Cibersegurança, no âmbito do Plano de Recuperação e Resiliência.

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Imagem do evento

Extended enrolement date until July 12th.

Logótipo do Workshop

A participação na 3.ª edição do Workshop é gratuita, mediante inscrição prévia.

Are you ready for this year's edition?

Imagem do evento - título, local e data do evento

Investigação Ecológica ao Serviço da Conservação

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.