Título
[pt] CÁLCULO DE SEQÜENTES DE SUCEDENTE MÚLTIPLO PARA LÓGICA INTUICIONISTA DE PRIMEIRA ORDEM
Título
[en] MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC
Autor
[pt] MARIA FERNANDA PALLARES COLOMAR
Vocabulário
[pt] TEORIA DA PROVA
Vocabulário
[pt] SUCEDENTE MULTIPLO
Vocabulário
[pt] CALCULO DE SEQUENCIAS
Vocabulário
[pt] GENTZEN
Vocabulário
[en] PROOF THEORY
Vocabulário
[en] MULTIPLE SUCCEDENT
Vocabulário
[en] SEQUENT CALCULUS
Vocabulário
[en] GENTZEN
Resumo
[pt] A primeira apresentação de um Cálculo de Seqüentes foi
feita por Gerhard Gentzen na década de 1930. Neste tipo de
sistema, a diferença entre as versões clássica e
intuicionista radicardinalidade do sucedente.
O sucedente múltiplo foi tradicionalmente considerado como
o elemento
que representava o aspecto clássico do sistema, enquanto
os seqüentes intuicionistas podiam ter, no máximo, uma
fórmula no sucedente. Nas décadas
seguintes foram formulados diversos cálculos
intuicionistas de sucedente
múltiplo que atenuaram essa restrição forte na
cardinalidade do sucedente.
Na década de 1990, estudou-se a relação de conexão ou
dependência entre
as fórmulas visando assegurar o caráter intuicionista dos
sistemas. Nós realizamos uma revisão dos sistemas de se
seqüentes intuicionistas e algumas das
suas aplicações. Apresentamos a versão do sistema FIL
(feita para o caso
proposicional por De Paiva e Pereira) para a lógica
intuicionista de primeira
ordem provando que o mesmo é correto, completo e satisfaz
eliminação de
corte.
Resumo
[en] The first Sequent Calculus was presented by Gerhard
Gentzen in
the thirties. In this system, the difference between
intuitionistic logic and
classical logic is based on the cardinality of the
succedent. Traditionally,
the multiple succedent was considered the element that
preserved the
classical aspect of the system, while intuitionistic
sequents have, at most,
one formula in the succedent. In the following decades,
several multiple
succedent intuitionistic calculus were presented that
diminish shed this st strong
restriction in the cardinality of the su succedent. In the
decade of 1990, this
cardinality restriction was replaced by a dependency
relation between the
formula ocurrences in the antecedent and in the succedent
of a sequent in
order to ensure the intuitionistic character of the
system. We make a revision
of the intuitionistic systems and some of their
applications. We present a
version of the system FIL (accomplish shed for the
propositional case by De
Paiva and Pereira) for first-order logic proving that it
is sound, complete
and that it satisfies the cut-elimination theorem.
Orientador(es)
LUIZ CARLOS PINHEIRO DIAS PEREIRA
Banca
EDWARD HERMANN HAEUSLER
Banca
LUIZ CARLOS PINHEIRO DIAS PEREIRA
Banca
OSWALDO CHATEAUBRIAND FILHO
Banca
WAGNER DE CAMPOS SANZ
Banca
MARIA DA PAZ NUNES DE MEDEIROS
Catalogação
2008-01-08
Apresentação
2007-06-26
Tipo
[pt] TEXTO
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Idioma(s)
PORTUGUÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=11144@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=11144@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.11144
Arquivos do conteúdo
CAPA, AGRADECIMENTOS, RESUMO, ABSTRACT E SUMÁRIO PDF CAPÍTULO 1 PDF CAPÍTULO 2 PDF CAPÍTULO 3 PDF CAPÍTULO 4 PDF REFERÊNCIAS BIBLIOGRÁFICAS E APÊNDICES PDF