A reasoning method for a paraconsistent logic (Q687160)

The recognition of the importance of paraconsistency for the study of the problem of modelling and automatizing the reasoning required to produce a glimmer of intelligent behavior on machines appeared in several previous works of the authors. This paper presents a proof method for automation of reasoning in the known paraconsistent predicate calculus \(C^*_ 1\) of da Costa. The method is analytical, using a specially designed tableau system. The reasoning method presented here is a tableau system sound and complete for \(C^*_ 1\), actually two tableau systems being developed. The system \(SC^*_ 1\) is presented with sketches for the proofs of its soundness and completeness with respect to the semantics of \(C^*_ 1\), being not suitable, meanwhile, for implementation. The system \(S'C^*_ 1\), a conservative extension of \(SC^*_ 1\) designed to enable better implementation, is then described. It has more rules, which prove to produce smaller trees than those resulting from the applications of the rules in \(SC^*_ 1\). The two systems are equivalent in the sense that they are able to prove the same theorems. A prototype based on \(S'C^*_ 1\) was effectively implemented and the authors suggest its improvement as a prover.