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.

翻译：受限非确定性矩阵（RNmatrix）对非确定性矩阵（Nmatrix）的行施加约束，过滤掉“非可靠”行并仅保留“有效”行，从而构建出比标准Nmatrix更具表达力的框架。尽管该方法能为广泛类别的逻辑（例如次协调逻辑、命题直觉主义逻辑以及模态立方体的十五种正规模态逻辑）提供可靠且完备的语义，但尚未有基于这些语义的高效判定过程被提出。本文实现了RNmatrix框架，为上述逻辑开发了一套新的自动定理证明工具。通过将RNmatrix及其消去准则编码为可满足性模理论（SMT）问题，我们利用SMT求解器判定公式有效性并构造反模型。在次协调逻辑中，我们的证明器超越了当前最先进水平，并为整个$C_n$层级提供了首个实现；在直觉主义逻辑与模态逻辑中，该通用证明器亦展现出具有竞争力的性能。