Doctoral Thesis
DOI
https://doi.org/10.11606/T.45.2007.tde-04052007-175943
Document
Author
Full name
Adolfo Gustavo Serra Seca Neto
E-mail
Institute/School/College
Knowledge Area
Date of Defense
Published
São Paulo, 2007
Supervisor
Committee
Finger, Marcelo (President)
Benevides, Mario Roberto Folhadela
Bittencourt, Guilherme
Carnielli, Walter Alexandre
Wassermann, Renata
Title in Portuguese
"Um provador de teoremas multi-estratégia"
Keywords in Portuguese
desenvolvimento de software
lógica clássica
lógica paraconsistente
lógicas de inconsistência formal
método dos tablôs
provadores de teoremas
Abstract in Portuguese
Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analÃtico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes caracterÃsticas: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponÃvel na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famÃlias de problemas; - sete famÃlias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famÃlias de problemas para avaliar provadores de teoremas paraconsistentes.
Title in English
A Multi-Strategy Tableau Prover
Keywords in English
classical logic
logics of formal inconsistency
paraconsistent logic
software development
tableau methods
theorem prover
Abstract in English
In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.
WARNING - Viewing this document is conditioned on your acceptance of the following terms of use:
This document is only for private use for research and teaching activities. Reproduction for commercial use is forbidden. This rights cover the whole data about this document as well as its contents. Any uses or copies of this document in whole or in part must include the author's name.
Publishing Date
2007-05-30