Verificação automática de lógicas finitas multivalentes

• Main Author: Sousa, Marcelo Rodrigues de
• Other Authors: Pereira, Antônio Eduardo Costa
• Format: Others
• Language: Portuguese
• Published: Universidade Federal de Uberlândia 2016
• Subjects: Lógica simbólica e matemática; CNPQ::ENGENHARIAS::ENGENHARIA ELETRICA
• Online Access: https://repositorio.ufu.br/handle/123456789/14268

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