Título
[en] A LABELLED NATURAL DEDUCTION LOGICAL FRAMEWORK
Título
[pt] UM FRAMEWORK LÓGICO PARA DEDUÇÃO NATURAL ROTULADA
Autor
[pt] BRUNO CUCONATO CLARO
Vocabulário
[pt] DEDUCAO NATURAL
Vocabulário
[pt] HASKELL
Vocabulário
[pt] SISTEMAS LOGICOS ROTULADOS
Vocabulário
[pt] SISTEMAS DEDUTIVOS ROTULADOS
Vocabulário
[pt] FRAMEWORK LOGICO
Vocabulário
[pt] ARCABOUCO LOGICO
Vocabulário
[pt] ASSISTENTE DE PROVAS
Vocabulário
[en] NATURAL DEDUCTION
Vocabulário
[en] HASKELL
Vocabulário
[en] LABELLED LOGICAL SYSTEMS
Vocabulário
[en] LABELLED DEDUCTIVE SYSTEMS
Vocabulário
[en] NATURAL DEDUCTION
Vocabulário
[en] LOGICAL FRAMEWORK
Vocabulário
[en] PROOF ASSISTANT
Resumo
[pt] Neste trabalho propomos um framework lógico para sistemas de Dedução
Natural rotulados. Sua meta-linguagem é baseada numa generalização dos
esquemas de regras propostos por Prawitz, e o uso de rótulos permite a
definição de lógicas intencionais como lógicas modais e de descrição, bem
como a definição uniforme de quantificadores como o para um número não-renumerável de indivíduos vale a propriedade P (lógica de Keisler), ou para
quase todos os indivíduos vale P (lógica de ultra-filtros), sem mencionar os
quantificadores padrões de lógica de primeira-ordem.
Mostramos também a implementação deste framework em um assistente
de prova virtual disponível livremente na web, e comparamos a definição
de sistemas lógicos nele com o mesmo feito em outros assistentes — Agda,
Isabelle, Lean, Metamath. Como subproduto deste experimento comparativo,
também contribuímos uma prova formal em Lean do postulado de Zolt em três
dimensões usando o sistema Zp proposto por Giovaninni et al.
Resumo
[en] We propose a Logical Framework for labelled Natural Deduction systems.
Its meta-language is based on a generalization of the rule schemas proposed by
Prawitz, and the use of labels allows the definition of intentional logics, such
as Modal Logic and Description Logic, as well as some quantifiers, such as
Keisler s for non-denumerable-many individuals property P, or for almost
all individuals P holds, or generally P holds, not to mention standard first-order logic quantifiers, all in a uniform way.
We also show an implementation of this framework as a freely-available
web-based proof assistant. We then compare the definition of logical systems
in our implementation and in other proof assistants — Agda, Isabelle, Lean,
Metamath. As a sub-product of this comparison experiment, we contribute a
formal proof (in Lean) of De Zolt s postulate for three dimensions, using the
Zp system proposed by Giovaninni et al.
Orientador(es)
EDWARD HERMANN HAEUSLER
Banca
EDWARD HERMANN HAEUSLER
Banca
LUIZ CARLOS PINHEIRO DIAS PEREIRA
Banca
JEFFERSON DE BARROS SANTOS
Banca
BRUNO LOPES VIEIRA
Banca
MARIO ROBERTO FOLHADELA BENEVIDES
Banca
JEAN-BAPTISTE JOINET
Catalogação
2023-11-27
Apresentação
2023-09-15
Tipo
[pt] TEXTO
Formato
application/pdf
Idioma(s)
INGLÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=65161@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=65161@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.65161
Arquivos do conteúdo
NA ÍNTEGRA PDF