Demonstração automática de teoremas em lógicas não clássicas : resolução assinalada para lógicas multivalentes

Abstract

As lógicas não clássicas são hoje essenciais no campo da matemática, quer pura quer aplicada. De entre estas, as lógicas multivalentes mostraram ser das mais importantes. A dedução automática, ou demonstração automática de teoremas, é hoje um requisito-chave em qualquer lógica, uma vez que as estratégias de dedução podem ser laboriosas e conter erros, em especial quando não se pode evitar níveis de alta complexidade. A automatização da dedução em lógica clássica quer proposicional quer de primeira ordem está já bastante desenvolvida e há hoje muitos demonstradores automáticos disponíveis. Contudo, o terreno das lógicas não clássicas só recentemente se tornou um objeto para a automatização da dedução e mostra-se muito desigualmente desbravado, com muito por investigar e fazer. Enquadrando a demonstração automática de teoremas nos problemas SAT e da decisão, nesta dissertação demonstramos que o cálculo de resolução é adequado, ou seja, correto e completo, para a automatização da demonstração de teoremas em lógicas multivalentes se aliado à lógica assinalada, constituindo assim a resolução assinalada para lógicas multivalentes. Demonstra-se ainda que este resultado vale para as lógicas finitamente multivalentes mais relevantes e para as quais existem sistemas axiomáticos adequados, bem como para alguns fragmentos de lógicas infinitamente ultivalentes, nomeadamente das lógicas conhecidas como difusas. Cimenta-se assim de forma segura a via para a investiga ção com vista à criação de software para a demonstração automática de teoremas em lógicas multivalentes por meio do cálculo de resolução.