Towards an efficient prover for the C1 paraconsistent logic
This work addresses a gap in automated reasoning for paraconsistent logics, which is incremental as it adapts an existing method to a specific logic.
The paper tackles the lack of a theorem prover for the C1 paraconsistent logic by presenting a sound and complete KE system and an informal strategy for implementation, aiming to benefit applications like robot control and medicine.
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 C1 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 C1, an informal specification of a strategy for the C1 prover as well as problem families that can be used to evaluate provers for C1. The C1 KE system and the strategy described in this paper will be used to implement a KE based prover for C1, which will be useful for those who study and apply paraconsistent logics.