A Polynomial Approach to Evidence: Algorithmic-Algebraic Methods for FDE and LETF

This paper characterises the Belnap-Dunn logic of first-degree entailment (FDE) and one of its extensions, the logic of evidence and truth (LETF ), by means of polynomials with coefficients in the ring Z2 . Two alternative algorithmic-algebraic methods for determining the deductive status of a formula with respect to a finite set of formulas in these logics are presented. The first method is based on the theory of Gröbner’s bases, while the second is based on Carnielli’s method of Polynomial Ring Calculus (PRC). Furthermore, it is noted that the satisfiability problem for these logics can also be solved using algebraic computation.