Título
[en] A GRAPH BASED THEOREM PROVING PLATFORM WITH STRATEGIES
Título
[pt] UMA PLATAFORMA DE DEMONSTRAÇÃO DE TEOREMAS BASEADA EM GRAFOS
Autor
[pt] BRUNO SCHROEDER
Vocabulário
[pt] LOGICA
Vocabulário
[pt] PROVADORES AUTOMATICOS DE TEOREMAS
Vocabulário
[pt] DEDUCOES ESTRUTURADAS COMO CIRCUITOS
Vocabulário
[pt] FERRAMENTAS PARA ESPECIFICACAO DE LOGICAS
Vocabulário
[pt] ASSISTENTES AUTOMATICOS DE DEMONSTRACAO
Vocabulário
[en] LOGIC
Resumo
[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.
Resumo
[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.
Orientador(es)
EDWARD HERMANN HAEUSLER
Banca
EDWARD HERMANN HAEUSLER
Banca
MARIO ROBERTO F BENEVIDES
Banca
GEIZA MARIA HAMAZAKI DA SILVA
Catalogação
2017-02-09
Apresentação
2008-08-13
Tipo
[pt] TEXTO
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Idioma(s)
INGLÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=29093@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=29093@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.29093
Arquivos do conteúdo
CAPA, AGRADECIMENTOS, ABSTRACT, RESUMO, SUMÁRIO E LISTA DE FIGURAS PDF CAPÍTULO 1 PDF CAPÍTULO 2 PDF CAPÍTULO 3 PDF CAPÍTULO 4 PDF CAPÍTULO 5 PDF CAPÍTULO 6 PDF BIBLIOGRAFIA E APÊNDICES PDF