[en] A LABELLED NATURAL DEDUCTION LOGICAL FRAMEWORK
Ano de defesa: | 2023 |
---|---|
Autor(a) principal: | |
Orientador(a): | |
Banca de defesa: | |
Tipo de documento: | Tese |
Tipo de acesso: | Acesso aberto |
Idioma: | eng |
Instituição de defesa: |
MAXWELL
|
Programa de Pós-Graduação: |
Não Informado pela instituição
|
Departamento: |
Não Informado pela instituição
|
País: |
Não Informado pela instituição
|
Palavras-chave em Português: | |
Link de acesso: | https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=65161&idi=1 https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=65161&idi=2 http://doi.org/10.17771/PUCRio.acad.65161 |
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. |