[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. / [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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:24302 |
| Date | 19 March 2015 |
| Creators | CECILIA REIS ENGLANDER LUSTOSA |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | English |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0026 seconds