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.
In this paper we present a new hierarchy of analytical tableaux systems TNDC"n,1@?n =1, as primitive operators, differently to what has been done in the literature, where these operators are usually defined operators. We prove a version of Cut Rule for the TNDC"n,1@?n<@w, and also prove that these systems are logically equivalent to the corresponding systems C"n,1@?n<@w. The systems TNDC"n constitute completely automated theorem proving systems for the systems of da Costa's hierarchy C"n,1@?n<@w.