Título: | MULTIPLE SUCCEDENT SEQUENT CALCULUS FOR INTUITIONISTIC FIRST-ORDER LOGIC | ||||||||||||||||||||||||||||||||
Autor: |
MARIA FERNANDA PALLARES COLOMAR |
||||||||||||||||||||||||||||||||
Colaborador(es): |
LUIZ CARLOS PINHEIRO DIAS PEREIRA - Orientador |
||||||||||||||||||||||||||||||||
Catalogação: | 08/JAN/2008 | Língua(s): | PORTUGUESE - BRAZIL |
||||||||||||||||||||||||||||||
Tipo: | TEXT | Subtipo: | THESIS | ||||||||||||||||||||||||||||||
Notas: |
[pt] Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
||||||||||||||||||||||||||||||||
Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=11144&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=11144&idi=2 |
||||||||||||||||||||||||||||||||
DOI: | https://doi.org/10.17771/PUCRio.acad.11144 | ||||||||||||||||||||||||||||||||
Resumo: | |||||||||||||||||||||||||||||||||
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.
|
|||||||||||||||||||||||||||||||||
|