In recent years, there is a growing interest in many-valued logics in many
areas such as computer sciences automated theorem proving, approximate
reasoning, multi-agent systems, program verication electrical engineering
and digital circuits, linguistics, mathematics and algebra, philosophy, etc.
In this context, the general problem of nding an axiomatization for nite
many-valued logics has not yet been solved satisfactorily. For this, we must
demonstrate the correction and completeness theorems of these logic systems,
both mathematically rigorous. Soundness theorem is straightforward,
however, it is known that the demonstration of the "completeness theorem"is
much more sosticated and unique for each logic system.
Completeness is one of the most important notions in logic and the foundations
of mathematics. Completeness means the possibility of getting all
correct and reliable schemata of inference by use of logical methods. When
one wishes to build or design a many-valued logic system, he or she is implicitly
looking for a system with a minimal set of axioms and rules.
The purpose of this thesis is to establish a general algorithmic completeness
proof procedure for nite many-valued logics. It is shown that a matrix
is characteristic (sound and complete) for a many-valued nite logic system
when, all successive correct extensions of this matrix have the same set of
tautologies. It is also shown that in order to determine if a matrix is characteristic, all one has to do is to fetch from all the unit extensions those
which are correct and then verify if they are repetitions of the matrix being
considered. How to implement a computational procedure to demonstrate
the completeness of a many-valued nite logic system is shown from these
results. The new approach is a simpler and more uniform solution for the
problem of nite many-valued logics axiomatization. / Nos últimos anos tem crescido o interesse nas denominadas lógicas multivalentes:
no ramo da computação, em áreas como prova automática de teoremas,
raciocínio aproximado, sistemas multi-agente e vericação de programas;
na engenharia elétrica como em circuitos digitais; na área da
matemática pura, como em provas de independência ou consistência, na teoria
generalizada de conjuntos e estruturas algébricas universais e mesmo na
linguística e losoa.
Nesse contexto, o problema de axiomatização geral de lógicas nitas multivalentes
ainda não foi resolvido de forma satisfatória. Para tal, devemos
demonstrar os teoremas da correção e completude desses sistemas lógicos,
ambos teoremas matematicamente rigorosos. De forma geral, a demostração
do teorema da correção não pode ser considerada como uma diculdade pois
é direta, bastando uma vericação nos axiomas e regras de inferência. No
entanto, é sabido que em geral a demonstração do teorema da completude
é muito mais sosticada e particular para cada sistema lógico.
A completude é uma das noções mais importantes na Lógica e nos fundamentos
da Matemática. Completude signica a demonstração da possibilidade
de obtermos todos os esquemas corretos de inferência através do
uso de um sistema formal lógico. Além disso, quando desejamos construir
ou desenhar um sistema lógico multivalente implicitamente estamos procurando por um sistema com um conjunto mínimo de axiomas e regras.
A proposta dessa tese é estabelecer um método algorítmico para demonstra
ção da completude em lógicas nitas multivalentes. Demonstra-se que se
uma matriz M é correta para um sistema lógico nito multivalente L e todas
as suas extensões unitárias corretas são repetições da matriz M, então
M é uma matriz característica de L. A partir desse resultado, são implementados
procedimentos computacionais que demonstram a completude de
um sistema lógico nito multivalente. A nova abordagem soluciona de uma
forma mais simples e uniforme o problema da axiomatização de lógicas nitas
multivalentes. / Doutor em Ciências
| Identifer | oai:union.ndltd.org:IBICT/urn:repox.ist.utl.pt:RI_UFU:oai:repositorio.ufu.br:123456789/14268 |
| Date | 08 April 2010 |
| Creators | Sousa, Marcelo Rodrigues de |
| Contributors | Pereira, Antônio Eduardo Costa, Souza, João Nunes de, Barbar, Jamil Salem, Soares, Alexsandro Santos, Lima-marques, Mamede |
| Publisher | Universidade Federal de Uberlândia, Programa de Pós-graduação em Engenharia Elétrica, UFU, BR, Engenharias |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFU, instname:Universidade Federal de Uberlândia, instacron:UFU |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0027 seconds