Efficient Decision Procedures for RNmatrix Semantics

TL;DR

This paper introduces an efficient decision procedure for RNmatrix semantics by encoding them as SMT problems, enabling automated theorem proving for various non-classical logics.

Contribution

It develops a novel SMT-based approach to decision procedures for RNmatrices, improving efficiency and enabling implementations for multiple logic systems.

Findings

Prover outperforms current state-of-the-art in paraconsistent logics.

First implementation for the entire Cn hierarchy of paraconsistent logics.

Achieves competitive performance for intuitionistic and modal logics.

Abstract

Restricted non-deterministic matrices (RNmatrices) impose constraints on the rows of non-deterministic matrices (Nmatrices), filtering out "unsound" rows and retaining only "valid" ones. This yields a more expressive framework than standard Nmatrices. Although this approach enables sound and complete semantics for a broad class of logics, \eg, paraconsistent logics, propositional intuitionistic logic, and the fifteen normal modal logics of the modal cube, no {\em efficient} decision procedures based on these semantics have been proposed. In this paper, we implement the RNmatrix framework to develop a new suite of automated theorem provers for these logics. By encoding RNmatrices and their elimination criteria as Satisfiability Modulo Theories (SMT) problems, we leverage SMT solvers to decide formula validity and construct countermodels. We illustrate the method for paraconsistent logics, where our prover outperforms the current state-of-the-art and provides the first implementation for the entire $C_n$ hierarchy, as well as for intuitionistic and modal logics, where our general-purpose prover achieves competitive performance.