Uma implementação do método das conexões de bibel para uma lógica paraconsistente anotada

Abstract

Resumo: O método das conexões de Bibel é uma alternativa ao método de resolução e vem sendo aplicado a vários sistemas lógicos, incluindo fragmentos da lógica linear, lógica intuicionista e várias lógicas modais. Em um trabalho anterior, o método das conexões de Bibel foi estendido para um tipo de lógica paraconsistente, chamada de lógica anotada. Neste trabalho o método do trabalho anterior é estendido tornando as definições mais adequadas à implementação. Um procedimento que melhora a eficiência do método das conexões de Bibel é apresentado e uma implementação do método é desenvolvida na linguagem SML. Os agentes inteligentes e sistemas especialistas podem utilizar métodos de prova em seus módulos raciocinadores para derivar conclusões de uma base de conhecimentos. A lógica anotada trata uma base de conhecimentos inconsistente de modo adequado. Um exemplo ilustrativo de uso de uma base de conhecimentos inconsistente em um sistema médico é automatizado através da implementação. Por fim, uma comparação de eficiência é apresentada.

Abstract: Bibel 's connection method is an alternative to the well know resolution method and has been applied in several logical systems, including fragments of linear logic, intuitionistic logic and various modal logics. In a previous work, Bibel's connection method was extended to a kind of paraconsistent logic, called annotated logic. In this work, the previous work is extended, making the definitions well suited for an implementation. A procedure that improve the efficiency is showed and an implementation in the Standard ML is developed. The intelligent agents and expertise systems can make use of proof methods in it's reasoning modules to derive conclusions of an knowledge base. The annotated logic can manage inconsistent knowledge bases in an adequate way. An illustrative example of the use of an inconsistent knowledge base in a medical system is automatized through the implementation. Finally, an efficiency comparai ion is showed.