Revisiting the proof theory of Classical S4

Barra lateral de artigos

Capa da revista O que nos faz pensar nº 39
PDF (English)
Publicado: dez. 30, 2016
Palavras-chave:
lógica modal, teoria da prova, normalização

Conteúdo do artigo principal

Bruno Lopes
Instituto de Computação da Universidade Federal Fluminense
Cecília Englander
Departamento de Informática da Pontifícia Universidade Católica do Rio de Janeiro
Fernanda Lobo
Marcela Cruz
Universidade Católica San Pablo

Resumo

Revisitando a teoria da prova de S4


1965, Dag Prawitz apresentou uma extensão dos sistemas tipo-Gentzen de Dedução Natural para os conceitos modais de S4. Maria da Paz Medeiros mostrou em 2006 que a prova de normalização para o S4 clássico não estava correta e propôs uma nova prova de normalização para um sistema logicamente equivalente, o sistema NS4. No entanto, dois problemas na prova do lema crítico usado por Medeiros em sua prova foram apontados por Yuuki Andou em 2009. Este artigo apresenta uma nova prova do lema crítico e, consequentemente, uma prova de normalização para NS4.
---
Artigo em inglês.

Detalhes do artigo

Edição
v. 25 n. 39 (2016): Filosofia, Lógica e Computação
Seção
Artigos

Nota de Direitos Autorais

O autor do artigo ou resenha submetido e aprovado para publicação autoriza os editores a reproduzi-lo e publicá-lo na a revista O que nos faz pensar, entendendo-se os termos "reprodução" e "publicação" conforme a licença Creative Commons Atribuição-NãoComercial 4.0 Internacional. O artigo ou resenha poderá ser acessado tanto pela rede mundial de computadores (WWW – Internet), como pela versão impressa, sendo permitidas, a título gratuito, a consulta e a reprodução do texto para uso próprio de quem a consulta. Essa autorização de publicação não tem limitação de tempo, ficando os editores da revista O que nos faz pensar responsável pela manutenção da identificação do autor do artigo.

Biografia do Autor

Bruno Lopes, Instituto de Computação da Universidade Federal Fluminense

Professor na Universidade Federal Fluminense (IC/UFF) e pesquisador no FR∀M∃ Lab. Já fui pesquisador visitante no Deduc˫eam/INRIA, com o qual desenvolvo parceria em conjunto com a Université Lyon 3 e com o TecMF/PUC-Rio. Minha principal linha de trabalho é na área de lógica para sistemas concorrentes mas também tenho trabalhado no desenvolvimento de provadores de teoremas extensíveis, normalização para sistemas de dedução natural, ontologias, formalização de sistemas multi-agentes e teoria da prova para lógicas.

Cecília Englander, Departamento de Informática da Pontifícia Universidade Católica do Rio de Janeiro

Possui graduação em Matemática pela Universidade Federal Fluminense (licenciatura e bacharelado, 2006) e mestrado e doutorado em Teoria da Computação pela Pontifícia Universidade Católica do Rio de Janeiro.

Fernanda Lobo

Possui graduação em Filosofia pela Universidade Federal do Rio de Janeiro (2006), mestrado em Lógica e Metafísica pela Universidade Federal do Rio de Janeiro (2009) e doutorado em Filosofia pela Pontifícia Universidade Católica do Rio de Janeiro (2015). Suas pesquisas enfatizam questões relacionadas às áreas de Filosofia da Lógica, Filosofia da Linguagem e Filosofia Antiga, principalmente nos seguintes temas: futuros contingentes, determinismo, bivalência, modalidades, tempo e lógicas aristotélica e estoica. Possui interesse na área de Ensino de Filosofia no nível médio.

Marcela Cruz, Universidade Católica San Pablo

Doutoranda em Informática pela Pontifícia Universidade Católica do Rio de Janeiro, mestrado em de Ciência da Computação pela Universidade Federal de Pernambuco. Possui graduação em Engenharia de Sistemas pela Universidad Nacional de San Agustín de Arequipa. Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Prova, Lógica e Sistemas de Prova.