Título
[pt] ALGUMAS RELAÇÕES ENTRE CÁLCULO DE SEQUENTES E DEDUÇÃO NATURAL
Título
[en] ON SOME RELATIONS BETWEEN NATURAL DEDUCTION AND SEQUENT CALCULUS
Autor
[pt] CECILIA REIS ENGLANDER LUSTOSA
Vocabulário
[pt] TEORIA DA PROVA
Vocabulário
[pt] LOGICA PROPOSICIONAL FINITO-VALORADA
Vocabulário
[pt] PROVA GERAL DA COMPLETUDE
Vocabulário
[pt] ISOMORFISMO
Vocabulário
[pt] CALCULO DE SEQUENTES
Vocabulário
[pt] DEDUCAO NATURAL
Vocabulário
[en] PROOF THEORY
Vocabulário
[en] FINITE-VALUED PROPOSITIONAL LOGIC
Vocabulário
[en] GENERAL COMPLETENESS PROOF
Vocabulário
[en] ISOMORPHISM
Vocabulário
[en] SEQUENT CALCULUS
Vocabulário
[en] NATURAL DEDUCTION
Resumo
[pt] Segerberg apresentou uma prova geral da completude para lógicas
proposicionais. Para tal, um sistema de dedução foi definido de forma que suas
regras sejam regras para um operador booleano arbitrário para uma dada lógica
proposicional. Cada regra desse sistema corresponde a uma linha na tabela de
verdade desse operador. Na primeira parte desse trabalho, mostramos uma
extensão da ideia de Segerberg para lógicas proposicionais finito-valoradas e
para lógicas não-determinísticas. Mantemos a ideia de definir um sistema de
dedução cujas regras correspondam a linhas de tabelas verdade, mas ao invés de
termos um tipo de regra para cada valor de verdade da lógica correspondente,
usamos uma representação bivalente que usa a técnica de fórmulas separadoras
definidas por Carlos Caleiro e João Marcos. O sistema definido possui tantas
regras que pode ser difícil trabalhar com elas. Acreditamos que um sistema
de cálculo de sequentes definido de forma análoga poderia ser mais intuitivo.
Motivados por essa observação, a segunda parte dessa tese é dedicada à
definição de uma tradução entre cálculo de sequentes e dedução natural, onde
procuramos definir uma bijeção melhor do que as já existentes.
Resumo
[en] Segerberg presented a general completeness proof for propositional logics.
For this purpose, a Natural Deduction system was defined in a way that its rules
were rules for an arbitrary boolean operator in a given propositional logic. Each
of those rules corresponds to a row on the operator s truth-table. In the first
part of this thesis we extend Segerbergs idea to finite-valued propositional logic
and to non-deterministic logic. We maintain the idea of defining a deductive
system whose rules correspond to rows of truth-tables, but instead of having
n types of rules (one for each truth-value), we use a bivalent representation
that makes use of the technique of separating formulas as defined by Carlos
Caleiro and João Marcos. The system defined has so many rules it might be
laborious to work with it. We believe that a sequent calculus system defined in
a similar way would be more intuitive. Motivated by this observation, in the
second part of this thesis we work out translations between Sequent Calculus
and Natural Deduction, searching for a better bijective relationship than those
already existing.
Orientador(es)
EDWARD HERMANN HAEUSLER
Coorientador(es)
GILLES DOWEK
Banca
EDWARD HERMANN HAEUSLER
Banca
LUIZ CARLOS PINHEIRO DIAS PEREIRA
Banca
GEIZA MARIA HAMAZAKI DA SILVA
Banca
WAGNER DE CAMPOS SANZ
Banca
GILLES DOWEK
Banca
JEAN BAPTISTE JOINET
Catalogação
2015-03-19
Apresentação
2014-07-08
Tipo
[pt] TEXTO
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Idioma(s)
INGLÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=24302@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=24302@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.24302
Arquivos do conteúdo
CAPA, AGRADECIMENTO, ABSTRACT, RESUMO E SUMÁRIO PDF CAPÍTULO 1 PDF CAPÍTULO 2 PDF CAPÍTULO 3 PDF CAPÍTULO 4 PDF CAPÍTULO 5 PDF CAPÍTULO 6 PDF REFERÊNCIAS BIBLIOGRÁFICAS PDF