[pt] Existem diferentes estilos de cálculos dedutivos, usados
para derivar os teoremas de uma lógica. Os mais habituais
são os sistemas axiomáticos; mas, do ponto de vista da
teoria da prova, os sistemas em dedução natural parecem
ser mais interessantes. Essa é a motivação que leva ao
desenvolvimento de técnicas que visam a facilitar a
transformação de um cálculo dedutivo para o estilo em
dedução natural. Esse trabalho se concentra no aspecto de
modelar regras para os quantificadores da linguagem
considerada e, para isso, faz uso de rótulos. Após uma
apresentação intuitiva da técnica desenvolvida, passa-se
à exposição de sistemas lógicos tratados pelo método:
lógica de ultrafiltros, lógica de filtros, CTL, lógica de
Keisler e CTL*. Em cada caso, analisam-se aspectos de
teoria da prova. / [en] There are many kinds of deductive calculus. The axiomatic
ones are the more usual. However, from the point of view of
proof theory, Natural Deduction systems seem to be more
interesting. This is the motivation for developping a
technique that aims to ease the transformation from
deductive calculus to Natural Deduction style. This work
concentrates on the aspect of modeling the rules for the
quantifiers of the logic considered, and for this purpose
labels are used. After an intuitive presentation of the
technique developped, some logical systems are treated by
the method: ultrafilter logic, filter logic, CTL, Keisler`s
logic and CTL*. For each one of them proof-theoretical
aspects are analysed.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:5508 |
| Date | 23 September 2004 |
| Creators | CHRISTIAN JACQUES RENTERIA |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | English |
| Type | TEXTO |
Page generated in 0.0016 seconds