[pt] ALGUMAS RELAÇÕES ENTRE CÁLCULO DE SEQUENTES E DEDUÇÃO NATURAL

• Ano de defesa: 2015
• Autor(a) principal: CECILIA REIS ENGLANDER LUSTOSA
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: MAXWELL
• Palavras-chave em Português: [pt] TEORIA DA PROVA; [pt] LOGICA PROPOSICIONAL FINITO-VALORADA; [pt] PROVA GERAL DA COMPLETUDE; [pt] ISOMORFISMO; [pt] CALCULO DE SEQUENTES; [pt] DEDUCAO NATURAL; [en] PROOF THEORY; [en] FINITE-VALUED PROPOSITIONAL LOGIC; [en] GENERAL COMPLETENESS PROOF; [en] ISOMORPHISM; [en] SEQUENT CALCULUS; [en] NATURAL DEDUCTION
• Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=24302&idi=1; https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=24302&idi=2; http://doi.org/10.17771/PUCRio.acad.24302

[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.