Made available in DSpace on 2014-12-17T15:47:50Z (GMT). No. of bitstreams: 1 JoseMS.pdf: 1057927 bytes, checksum: 2fb0b885cdff7c8f9e8f9d1d07d2627f (MD5) Previous issue date: 2001-07-17 / The intervalar arithmetic well-known as arithmetic of Moore, doesn't possess the same properties of the real numbers, and for this reason, it is confronted with a problem of operative nature, when we want to solve intervalar equations as extension of real equations by the usual equality and of the intervalar arithmetic, for this not to possess the inverse addictive, as well as, the property of the distributivity of the multiplication for the sum doesn t be valid for any triplet of intervals. The lack of those properties disables the use of equacional logic, so much for the resolution of an intervalar equation using the same, as for a representation of a real equation, and still, for the algebraic verification of properties of a computational system, whose data are real numbers represented by intervals. However, with the notion of order of information and of approach on intervals, introduced by Aci?ly[6] in 1991, the idea of an intervalar equation appears to represent a real equation satisfactorily, since the terms of the intervalar equation carry the information about the solution of the real equation. In 1999, Santiago proposed the notion of simple equality and, later on, local equality for intervals [8] and [33]. Based on that idea, this dissertation extends Santiago's local groups for local algebras, following the idea of Σ-algebras according to (Hennessy[31], 1988) and (Santiago[7], 1995). One of the contributions of this dissertation, is the theorem 5.1.3.2 that it guarantees that, when deducing a local Σ-equation E t t in the proposed system SDedLoc(E), the interpretations of t and t' will be locally the same in any local Σ-algebra that satisfies the group of fixed equations local E, whenever t and t have meaning in A. This assures to a kind of safety between the local equacional logic and the local algebras / A aritm?tica intervalar conhecida como aritm?tica de Moore, n?o possui as mesmas propriedades dos n?meros reais, e por este motivo, defrontase com um problema de natureza operat?ria, quando se deseja resolver equa??es intervalares como extens?o de equa??es reais atrav?s da igualdade usual e da aritm?tica intervalar, por esta n?o possuir o inverso aditivo, como tamb?m, a propriedade da distributividade da multiplica??o pela soma n?o ser v?lida para qualquer terno de intervalos. A falta dessas propriedades impossibilita a utiliza??o da l?gica equacional, tanto para a resolu??o de uma equa??o intervalar usando a mesma, como para uma representa??o de uma equa??o real, e ainda, para a verifica??o alg?brica de propriedades de um sistema computacional, cujos dados sejam n?meros reais representados atrav?s de intervalos. Entretanto, com a no??o de ordem de informa??o e de aproxima??o sobre intervalos, introduzida por Aci?ly[6] em 1991, surge a id?ia de uma equa??o intervalar representar satisfatoriamente uma equa??o real, j? que os termos da equa??o intervalar carregam a informa??o sobre a solu??o da equa??o real. Em 1999, Santiago prop?s a no??o de igualdade simples e, posteriormente, igualdade local para intervalos [8] e [33]. Baseado nessa id?ia, esta disserta??o estende os conjuntos locais de Santiago para ?lgebras locais, seguindo a id?ia de Σ-?lgebras contidas em (Hennessy[31], 1988) e (Santiago[7], 1995). Uma das contribui??es desta disserta??o ? o teorema 5.1.3.2 que garante que, ao se deduzir uma Σ-equa??o local ⊢ E t t no sistema SDedLoc(E) proposto, as interpreta??es de t e t ser?o localmente iguais em qualquer Σ-?lgebra local que satisfa?a o conjunto de equa??es locais E fixado, sempre que t e t tiverem significado em A. Isto garante um tipo de seguran?a entre a l?gica equacional local e as ?lgebras locais

[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.