Seminário remoto "Lógicos em Quarentena" 05/11/2020 (quinta-feira) 16:00h
19 views
Skip to first unread message
Bruno Lopes
Nov 2, 2020, 6:01:47 AM11/2/20
to Sociedade Brasileira de Computação, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA, logi...@sbc.org.br
Numa iniciativa conjunta da Sociedade Brasileira de Lógica e do Grupo de Interesse em Lógica da Sociedade Brasileira de Computação, gostaríamos de convidar a todos a participarem do Seminário "Lógicos em Quarentena". Trata-se de um seminário remoto com apresentações informais por membros da comunidade e espaço para perguntas no fim. As apresentações usualmente são gravadas e disponibilizadas na página do evento http://lq.sbl.org.br (com a agenda completa).
Data: 05 de novembro de 2020 (quinta-feira)
Horário: 16:00h GMT-3
Apresentador: Carlos Olarte (ECT/UFRN)
Título: The L-Framework*: Structural Proof Theory in Rewriting Logic
Resumo: Structural properties such as admissibility and invertibility of rules are crucial in proof theory, and they can be used for establishing other key properties such as cut-elimination and completeness of focusing in sequent systems. Finding proofs for these properties requires inductive reasoning over the provability relation, which is often quite elaborated, exponentially exhaustive, and error prone. We propose automatic procedures for proving structural properties of sequent systems. Our techniques are based on the rewriting logic metalogical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in Maude and the resulting framework is generic and modular since cut-freeness, admissibility, and invertibility can be proved incrementally. The L-Framework achieves a great degree of automation when used on several sequent systems. Case studies include intuitionistic, classical, substructural and modal logics.
* https://carlosolarte.github.io/L-framework/
A apresentação ocorrerá pelo Google Meet através do link público https://meet.google.com/pkq-fxvz-iou .
Data: 05 de novembro de 2020 (quinta-feira)
Horário: 16:00h GMT-3
Apresentador: Carlos Olarte (ECT/UFRN)
Título: The L-Framework*: Structural Proof Theory in Rewriting Logic
Resumo: Structural properties such as admissibility and invertibility of rules are crucial in proof theory, and they can be used for establishing other key properties such as cut-elimination and completeness of focusing in sequent systems. Finding proofs for these properties requires inductive reasoning over the provability relation, which is often quite elaborated, exponentially exhaustive, and error prone. We propose automatic procedures for proving structural properties of sequent systems. Our techniques are based on the rewriting logic metalogical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in Maude and the resulting framework is generic and modular since cut-freeness, admissibility, and invertibility can be proved incrementally. The L-Framework achieves a great degree of automation when used on several sequent systems. Case studies include intuitionistic, classical, substructural and modal logics.
* https://carlosolarte.github.io/L-framework/
A apresentação ocorrerá pelo Google Meet através do link público https://meet.google.com/pkq-fxvz-iou .
Bruno Lopes
Professor Adjunto
Instituto de Computação
Universidade Federal Fluminense
Reply all
Reply to author
Forward
0 new messages