The KE inference system is a tableau method developed by Marco Mondadori which was presented as an improvement, in the computational efficiency sense, over Analytic Tableaux. In the literature, there is no description of a theorem prover based on the KE method for the C"1 paraconsistent logic. Paraconsistent logics have several applications, such as in robot control and medicine. These applications could benefit from the existence of such a prover. We present a sound and complete KE system for C"1, an informal specification of a strategy for the C"1 prover as well as problem families that can be used to evaluate provers for C"1. The C"1KE system and the strategy described in this paper will be used to implement a KE based prover for C"1, which will be useful for those who study and apply paraconsistent logics.
Segundo a pressuposicao de consistencia classica, as contradicoes tem um cara[c]ter explosivo; uma vez que estejam presentes em uma teoria, tudo vale, e nenhum raciocinio sensato pode entao ter lugar. Uma logica e paraconsistente se ela rejeita uma tal pressuposicao, e aceita ao inves que algumas teorias inconsistentes conquanto nao-triviais facam perfeito sentido. A? Logicas da Inconsistencia Formal, LIFs, formam uma classe de logicas paraconsistentes particularmente expressivas nas quais a nocao meta-teonca de consistencia pode ser internalizada ao nivel da linguagem obje[c]to. Como consequencia, as LIFs sao capazes de recapturar o raciocinio consistente pelo acrescimo de assuncoes de consistencia apropriadas. Assim, por exemplo, enquanto regras classicas tais como o silogismo disjuntivo (de A e nao-,4)-ou-13, infira B) estao fadadas a falhar numa logica paraconsistente (pois A e (nao-A) poderiam ambas ser verdadeiras para algum A, independentemente de B), elas podem ser recuperadas por uma LIF se o conjunto das premissas for ampliado pela presuncao de que estamos raciocinando em um ambiente consistente (neste caso, pelo acrescimo de (consistente-.A) como uma hipotese adicional da regra). A presente monografia introduz as LIFs e apresenta diversas ilustracoes destas logicas e de suas propriedades, mostrando que tais logicas constituem com efeito a maior parte dos sistemas paraconsistentes da literatura. Diversas formas de se efe[c]tuar a recaptura do raciocinio consistente dentro de tais sistemas inconsistentes sao tambem ilustradas Em cada caso, interpretacoes em termos de semânticas polivalentes, de traducoes possiveis ou modais sao fornecidas, e os problemas relacionados a provisao de contrapartidas algebricas para tais logicas sao examinados. Uma abordagem formal abstra[cjta e proposta para todas as definicoes relacionadas e uma extensa investigacao e feita sobre os principios logicos e as propriedades positivas e negativas da negacao Abstract