A reduction-based theorem prover for 3-valued logic.
We present a new prover for propositional 3-valued logics, TAS-M3, which is an extension of the TAS-D prover for classical propositional logic. TAS-M3 uses the TAS methodology and, consequently, it is a reduction-based method. Thus, its power is based on the reductions of the size of the formula executed by the F transformation. This transformation dynamically filters the information contained in the syntactic structure of the formula to avoid as much distributions as possible, in order to improve...