[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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:29093 |
| Date | 09 February 2017 |
| Creators | BRUNO SCHROEDER |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | English |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0018 seconds