[pt] Demonstrações em lógica podem tornar-se muito grandes e complexas. Para resolver problemas, e para estudar lógica, é comum valer-se de assistentes de demonstração. Um assistente de demonstração geral deve integrar ferramentas que ajudem a especificar as lógicas, as equações, os conjuntos de regras, e as estratégias de busca (semi) automática de demonstrações. A comunidade usuária de Provadores Automáticos de Teoremas conhece algumas ferramentas que atendem a estes requisitos. Entretanto, estas ferramentas não estão preparadas para lidar com demonstrações muito grandes. Trabalhos recentes sugerem que uma boa forma de chegar a demonstrações menores é usar grafos, ao invés de árvores, para representar demonstrações. Esta dissertação descreve e implementa uma máquina virtual baseada em grafo e um compilador para a confecção de provadores de teoremas baseados em grafo. Para validar a ferramenta, alguns estudos de casos e provadores de teoremas baseados em grafo são apresentados. / [en] Proofs in logic can become very big and complex. For problem solving, and to teach logic, it is common the use of proof assistants. A general proof assistant should integrate tools to help users on specifying the logics, the formulas, the sets of rules, and the very strategy to perform (semi) automatic proof search. The Automatic Theorem Provers community is aware of some tools that were designed to fulfill these requirements. However, these tools do not take the (possibly) huge size of a proof. Recent works have pointed out that a good way to achieve shorter proofs is the use of graphs, instead of trees, to represent proofs. This dissertation describes and implements a graph-based virtual machine and a compiler for the production of graph-based theorem provers. Some case studies, standard as well as graph-based theorem prover, are illustrated in order to validate the tool.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2010 / Made available in DSpace on 2013-07-16T04:00:47Z (GMT). No. of bitstreams: 1 284644.pdf: 1072188 bytes, checksum: 9661a4bf4e0a1b281204cdd75b75e0fd (MD5) / Em sistemas de tempo real, as tarefas devem executar em um período de tempo previsível e sem atrasos, para assim garantir o bom funcionamento do sistema. Este trabalho trata sobre o que ocorre no Linux com a utilização do pacote de tempo real PREEMPT-RT. O problema encontrado é uma inversão de prioridades que os processos de tempo real sofrem, a qual ocorre através da execução de alguns temporizadores de alta resolução, mais especificamente, os temporizadores responsáveis por acordar os processos que estavam dormindo por um certo período de tempo. Quando estes processos precisam acordar, os temporizadores preemptam qualquer processo em execução para isto. Neste caso, processos de menor prioridade interferem na execução de processos com maior prioridade. Para resolver este problema, este trabalho propõe a postergação da execução destes temporizadores, os executando em momentos apropriados, de forma que respeitem as prioridades dos processos e não posterguem demais o início da execução dos processos que devem acordar.