Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2009. / Submitted by Marília Freitas (marilia@bce.unb.br) on 2011-05-04T19:47:15Z No. of bitstreams: 1 2009_AndreiaBorgesAvelar.pdf: 569913 bytes, checksum: b9c7b5fd67d3f7351a8c69fe64218b4a (MD5) / Approved for entry into archive by Daniel Ribeiro(daniel@bce.unb.br) on 2011-05-07T01:10:24Z (GMT) No. of bitstreams: 1 2009_AndreiaBorgesAvelar.pdf: 569913 bytes, checksum: b9c7b5fd67d3f7351a8c69fe64218b4a (MD5) / Made available in DSpace on 2011-05-07T01:10:24Z (GMT). No. of bitstreams: 1 2009_AndreiaBorgesAvelar.pdf: 569913 bytes, checksum: b9c7b5fd67d3f7351a8c69fe64218b4a (MD5) / Neste trabalho apresenta-se uma formalização do teorema de existência de unificadores mais gerais em teorias de primeira ordem. Tal formalização foi desenvolvida na linguagem de especificação de ordem superior, do assistente de prova PVS. A prova mecânica e muito semelhante as provas encontradas em livros-texto, as quais se baseiam na correção do já conhecido algoritmo de unificação de Robinson de primeira ordem. A prova do teorema foi aplicada dentro de uma teoria completa, desenvolvida em PVS, para sistemas de reescrita de termos, a m de obter uma formalização completa do Teorema dos Pares Críticos de Knuth-Bendix. Para chegar a esta formalização foi construída uma especificação em PVS de uma teoria para unificação de primeira ordem, onde foram formalizadas as propriedades de generalidade e terminação de uma versão do algoritmo de unificação de Robinson restrito a termos unificáveis. _________________________________________________________________________________ ABSTRACT / This work presents the formalization of the theorem of existence of most general unifiers in first-order theories. The formalization was developed in the higher-order speciation language, of the proof assistant PVS. The mechanical proof is very similar to that found in textbooks, which are based on proving the correction of the well-known Robinson's first-order unification algorithm. The proof of the theorem was applied within a complete theory, also developed in PVS, for term rewriting systems in order to obtain the full formalization of the Knuth-Bendix Critical Pair theorem. To reach this formalization, it was build in PVS a specification of a theory first-order unification, where properties of generality and termination of a version of the Robinson's unification algorithm restricted to unifiable terms were formalized.

SILVA, Hugo Victor. Solução de sistemas lineares através do método computacional para alunos da educação básica. 2013. 41 f. Dissertação (Mestrado em Matemática em Rede Nacional) – Centro de Ciências, Universidade Federal do Ceará, Fortaleza, 2013. / Submitted by Rocilda Sales (rocilda@ufc.br) on 2013-10-29T12:39:07Z No. of bitstreams: 1 2013 _dis_hvsilva.PDF: 1164060 bytes, checksum: 05269677b8b99860a783b53903e921d8 (MD5) / Approved for entry into archive by Rocilda Sales(rocilda@ufc.br) on 2013-10-29T12:39:40Z (GMT) No. of bitstreams: 1 2013 _dis_hvsilva.PDF: 1164060 bytes, checksum: 05269677b8b99860a783b53903e921d8 (MD5) / Made available in DSpace on 2013-10-29T12:39:41Z (GMT). No. of bitstreams: 1 2013 _dis_hvsilva.PDF: 1164060 bytes, checksum: 05269677b8b99860a783b53903e921d8 (MD5) Previous issue date: 2013 / Systems of linear equations are a topic covered in high school so limited mainly due to the excess calculations to be made to find a whole solution. This dissertation aims to create and provide a tool for teachers who are interested in teaching find the solution of several linear systems to their basic education students using computational logic as this work contains tools for introducing the study of computational logic ally a simple programming language, accessible to students both as a regular high school for technology education. Furthermore, we present an interesting application in one of the traditional problems of chemistry, balancin reactions. In this thesis we will also address some necessary definitions and operations involving matrices. Moreover, we will see how to use a simple programming language that is used as a tool for initial learning in most courses basic programming language, the Structured Portuguese. We will point some elements of syntax VisuAlg 2.5, free compiler and auto executable that will help us achieve our goal. We will see how to find the solution of a system of linear equations with a finite number of variables using the method of scheduling systems, the backward substitution and following an algorithm for finding such a solution. / Sistemas de equações lineares é um tema abordado no ensino médio de forma limitada principalmente por conta do excesso de cálculos a serem feitos para encontrar seu conjunto solução. A presente dissertação tem como objetivo criar e disponibilizar uma ferramenta aos professores que têm interesse em ensinar a encontrar a solução de sistemas lineares diversos aos seus alunos da educação básica utilizando a lógica computacional já que este trabalho contém ferramentas para a introdução do estudo de lógica computacional aliada a uma linguagem de programação simples e acessível aos estudantes tanto para o ensino médio regular como para a educação tecnológica. Além disso, apresentamos uma interessante aplicação em um dos problemas tradicionais da química, o balanceamento de reações. Nesta dissertação, também faremos uma abordagem de algumas definições necessárias envolvendo matrizes e suas operações. Além disso, veremos como utilizar uma linguagem de programação simples que é usada como ferramenta de aprendizagem inicial na maioria dos cursos básicos de linguagem de programação, o Português Estruturado. Pontuaremos alguns elementos da sintaxe do VisualG 2.5, compilador gratuito e autoexecutável que irá nos ajudar a atingir nosso objetivo. Veremos como encontrar a solução de um sistema de equações lineares com um número finito de variáveis usando o método do escalonamento de sistemas, a substituição retroativa e seguindo um algoritmo computacional para chegar a tal solução

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2008. / Submitted by Diogo Trindade Fóis (diogo_fois@hotmail.com) on 2009-10-09T14:02:12Z No. of bitstreams: 1 2008_RommelNovaesCarvalho_reduzida.pdf: 2306641 bytes, checksum: a442bd9631a732feaae059332a6a5068 (MD5) / Approved for entry into archive by Gomes Neide(nagomes2005@gmail.com) on 2010-10-15T14:38:05Z (GMT) No. of bitstreams: 1 2008_RommelNovaesCarvalho_reduzida.pdf: 2306641 bytes, checksum: a442bd9631a732feaae059332a6a5068 (MD5) / Made available in DSpace on 2010-10-15T14:38:05Z (GMT). No. of bitstreams: 1 2008_RommelNovaesCarvalho_reduzida.pdf: 2306641 bytes, checksum: a442bd9631a732feaae059332a6a5068 (MD5) Previous issue date: 2008-02-29 / O objetivo geral deste trabalho é pesquisar formalismos para extensão de redes bayesianas (BN) e raciocínio plausível na Web Semântica. Dentre os formalismos para raciocínio plausível, um dos mais utilizados, dada sua flexibilidade, é a rede bayesiana. No entanto, há diversas situações do mundo real e na Web que as BN são incapazes de representar. As duas principais restrições de redes bayesianas são a impossibilidade de representar recursão e situações onde o número de variáveis aleatórias envolvidas é desconhecido. Exatamente para superar essas limitações que utilizaremos o formalismo MEBN (Multi-Entity Bayesian Network), que agrega o poder de expressividade da lógica de primeira ordem (FOL) às redes bayesianas, possibilitando a representação de um número infinito de variáveis aleatórias e a representação de definições recursivas. Na Web Semântica, a linguagem OWL (Ontology Web Language) permite a definição de ontologias, mas por ser baseada na FOL não possui um suporte adequado para possibilitar o raciocínio plausível. Por ser uma implementação de lógica probabilística de primeira ordem, a MEBN é um dos formalismos mais indicados para tal expansão, tendo a linguagem PR-OWL (Probabilistic OWL) sido proposta como uma integração de MEBN e OWL [29, 28, 27]. O presente trabalho de pesquisa propõe alguns refinamentos do formalismo MEBN e da linguagem PR-OWL e apresenta a primeira implementação no mundo de MEBN com a possibilidade de representar e raciocinar em domínios com incerteza através de ontologias probabilísticas baseadas em PR-OWL. Além disso, um novo algoritmo para geração de SSBN (Situation-Specific Bayesian Network) foi proposto. Essa implementação foi feita no UnBBayes [26], ferramenta livre para raciocínio probabilístico, aproveitando o mecanismo de criação e inferência de BN que esta já possui. Para exemplificar uma aplicação de MEBN/PR-OWL, o UnBBayes-MEBN [6] foi utilizado para modelar e raciocinar no domínio fictício Star Trek. Como ontologias probabilísticas possuem um grande potencial de uso no campo da Web Semântica onde a incerteza é tratada de forma probabilística, essa pesquisa representa uma contribuição para os trabalhos que estão sendo realizados pelo URW3-XG (W3C Uncertainty Reasoning for the World Wide Web Incubator Group) [30], criado pelo Consórcio World Wide Web para melhor definir o desafio de representar e raciocinar com a informação incerta disponível na Web. _________________________________________________________________________________ ABSTRACT / The general objective of this work is to research formalisms for extending Bayesian networks (BN) and plausible reasoning in the Semantic Web. Among the formalisms for plausible reasoning, one of the most used, given its flexibility, is BN. However, there are several situations in the real world and in the Web that BN is unable to represent. The two main restrictions of BN are the impossibility of representing recursion and situations where the number of random variables is unknown. It is exactly to overcome those limitations that we will use the MEBN formalism (Multi-Entity Bayesian Network), which joins the expressiveness power of first order logic (FOL) to BN, making possible the representation of an infinite number of random variables and of recursive definitions. In Semantic Web, the OWL language (Ontology Web Language) allows the definition of ontologies, but because it is based in FOL it doesn’t possess an appropriate support to make the plausible reasoning possible. MEBN is one of the most suitable formalisms for such expansion, as it is an implementation of first order probabilistic logic, having the PR-OWL language (Probabilistic OWL) as an integration of MEBN and OWL [29, 28, 27]. This research proposes some refinements for the MEBN formalism and PR-OWL language and it presents the first implementation in the world of MEBN with the possibility to represent and reason in domains with uncertainty through probabilistic ontologies based in PR-OWL. Besides that, a new algorithm for the SSBN generation was proposed. This implementation was made in UnBBayes [26], a free tool for probabilistic reasoning, taking advantage of the BN modeling and inference mechanism that it already has. To exemplify an application of MEBN/PR-OWL, UnBBayes-MEBN [6] was used to model and to reason in the Star Trek toy domain. As probabilistic ontologies have a great potential use in the field of Semantic Web where the uncertainty is treated in a probabilistic way, this research represents a contribution for the work that is being accomplished by the URW3-XG (W3C Uncertainty Reasoning for the World Wide Web Incubator Group) [30], created by the World Wide Web Consortium for best defining the challenge of representing and reasoning with the available uncertain information in the Web.

No description available.