Return to search

Dedução automática por tableaux estruturada em XML

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-20T10:56:48Z (GMT). No. of bitstreams: 1
197133.pdf: 2644540 bytes, checksum: a258dbeabb2ac6818b4802500a65e309 (MD5) / Este trabalho tem como objetivo descrever o desenvolvimento de um provador de teoremas segundo o Método dos Tableaux. Para isso, foram propostos dois refinamentos com o intuito de tornar o método mais eficiente durante as etapas de prova. Esses refinamentos tratam da ordenação das fórmulas e da instanciação das variáveis, buscando diminuir a inserção de elementos na árvore, propiciando, assim, uma maior eficiência em relação ao número de nós. A linguagem Java foi utilizada para a implementação do provador, possibilitando a manipulação das fórmulas estruturadas como documentos XML. Ao final do trabalho, é verificada a eficiência do provador através da comparação com outros provadores em relação à sistematização das suas etapas de prova e dos resultados obtidos.

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/84615
Date January 2003
CreatorsBrito, Parcilene Fernandes de
ContributorsUniversidade Federal de Santa Catarina, Buchsbaum, Arthur Ronald de Vallauris
PublisherFlorianópolis, SC
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Formatxiv, 108 f.| il.
Sourcereponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0017 seconds