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.

翻译：受限非确定性矩阵（RN矩阵）对非确定性矩阵（N矩阵）的行施加约束，过滤掉"非健全"行，仅保留"有效"行。这构建了比标准N矩阵更具表达力的框架。尽管该方法能为广泛逻辑类（包括次协调逻辑、命题直觉主义逻辑以及模态立方体中十五种正规模态逻辑）提供健全且完备的语义，但尚无基于这些语义的"高效"判定程序被提出。本文通过实现RN矩阵框架，为这些逻辑开发了一套新型自动定理证明器。通过将RN矩阵及其消去准则编码为可满足性模理论（SMT）问题，我们利用SMT求解器判定公式有效性并构建反模型。针对次协调逻辑的实证表明，我们的证明器优于现有最优方案，且首次为整个$C_n$层级提供了实现；针对直觉主义逻辑和模态逻辑，我们的通用证明器也展现出具有竞争力的性能。