Sistemas dedutivos no estilo de dedução natural e cálculo de sequentes para "Geralmente"
14 Junho 2012 ·
- Quem: Leonardo Vana
- Onde: FGV -- Praia de Botafogo, 190, sala 317
- Quando: 14 de Junho de 2012 às 16:00h
Afirmações que contêm noções vagas, tais como “geralmente”, “muitos”, “raramente” etc. ocorrem freqüentemente em linguagem natural e em vários ramos da ciência. Por outro lado, procedimentos de construção de provas, muitas vezes chamados provadores automáticos de teoremas, tem sido objeto de estudo de pesquisadores em diversas áreas. Diferentes formalismos lógicos têm sido utilizados como base para provadores, tais como cálculo de seqüentes, dedução natural e os métodos de resolução e de tableaux. As Lógicas de “Geralmente” captam as distintas noções de “geralmente” e são obtidas estendendo a Lógica de Primeira Ordem pela introdução de um novo quantificador \( \nabla \) para representar “geralmente”, “muitos” etc. Intuitivamente, o quantificador \(\nabla\) é utilizado para expressar “objetos geralmente têm uma dada propriedade.” Os sistemas dedutivos no estilo de dedução natural e cálculo de seqüentes para as Lógicas de “Geralmente” são construídos com a adição de regras que refletem as distintas noções de “geralmente” nos sistemas dedutivos originalmente desenvolvidos para a Lógica de Primeira Ordem. Os resultados de corretude e completude dos sistemas dedutivos para as Lógicas de “Geralmente” são obtidos em relação aos sistemas dedutivos para a Lógica de Primeira Ordem. Para os sistemas no estilo de dedução natural para as Lógicas de “Geralmente” demonstramos o resultado de normalização e caracterizamos a estrutura das provas normais. Nos sistemas no estilo de cálculo de seqüentes identificamos exatamente as aplicações da regra do corte que não podem ser eliminadas.
Observação para visitantes
A presença é gratuíta e não exige confirmação. A FGV não permite a entrada de homens vestindo bermuda ou chinelo.