[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. / [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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:65161 |
| Date | 27 November 2023 |
| Creators | BRUNO CUCONATO CLARO |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | English |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0024 seconds