A semantic tableau version of first-order quasi-classical logic

Abstract

Quasi-classical logic (QC logic) allows the derivation of non-trivial classical inferences from inconsistent information. A paraconsistent, or non-trivializable, logic is, by necessity, a compromise, or weakening, of classical logic. The compromises on QC logic seem to be more appropriate than other paraconsistent logics for applications in computing. In particular, the connectives behave in a "classical manner" at the object level so that important proof rules such as modus tollens, modus ponens, and disjunctive syllogism hold. Here we develop QC logic by presenting a semantic tableau version for FIrst-order QC logic.