Abstracts Category : Other

[en] A GRAPH BASED THEOREM PROVING PLATFORM WITHSTRATEGIES

by SCHROEDER BRUNO

[pt] Demonstraes em lgica podem tornar-se muitograndes e complexas. Para resolver problemas, e para estudarlgica, comum valer-se de assistentes de demonstrao. Umassistente de demonstrao geral deve integrar ferramentas queajudem a especificar as lgicas, as equaes, os conjuntos deregras, e as estratgias de busca (semi) automtica dedemonstraes. A comunidade usuria de Provadores Automticos deTeoremas conhece algumas ferramentas que atendem a estesrequisitos. Entretanto, estas ferramentas no esto preparadas paralidar com demonstraes muito grandes. Trabalhos recentes sugeremque uma boa forma de chegar a demonstraes menores usar grafos,ao invs de rvores, para representar demonstraes. Estadissertao descreve e implementa uma mquina virtual baseada emgrafo e um compilador para a confeco de provadores de teoremasbaseados em grafo. Para validar a ferramenta, alguns estudos decasos e provadores de teoremas baseados em grafo soapresentados. [en] Proofs in logic can become very big and complex.For problem solving, and to teach logic, it is common the use ofproof assistants. A general proof assistant should integrate toolsto help users on specifying the logics, the formulas, the sets ofrules, and the very strategy to perform (semi) automatic proofsearch. The Automatic Theorem Provers community is aware of sometools that were designed to fulfill these requirements. However,these tools do not take the (possibly) huge size of a proof. Recentworks have pointed out that a good way to achieve shorter proofs isthe use of graphs, instead of trees, to represent proofs. Thisdissertation describes and implements a graph-based virtual machineand 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.Advisors/Committee Members: EDWARD HERMANN HAEUSLER.