Towards an efficient prover for the C1 paraconsistent logic

TL;DR

This paper introduces a sound and complete KE inference system tailored for the C1 paraconsistent logic, aiming to improve computational efficiency and facilitate applications in fields like robotics and medicine.

Contribution

It presents the first KE-based theorem prover for C1, including a strategy and evaluation problem families, advancing tools for paraconsistent logic applications.

Findings

Developed a sound and complete KE system for C1

Proposed a strategy for implementing the C1 prover

Identified problem families for evaluating C1 provers

Abstract

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.