pith. machine review for the scientific record. sign in

arxiv: 2605.01845 · v2 · submitted 2026-05-03 · 💻 cs.LO

Recognition: unknown

Efficient Decision Procedures for RNmatrix Semantics

Carlos Olarte, Elaine Pimentel, Renato R. Leme

Pith reviewed 2026-05-09 16:30 UTC · model grok-4.3

classification 💻 cs.LO
keywords RNmatricesSMT solversparaconsistent logicsdecision proceduresautomated theorem provingintuitionistic logicmodal logicscountermodel generation
0
0 comments X

The pith

Encoding RNmatrices as SMT problems produces practical decision procedures for paraconsistent, intuitionistic and modal logics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that restricted non-deterministic matrices can be turned into automated theorem provers by translating both their truth tables and the rules that eliminate unsound rows into constraints solvable by off-the-shelf SMT solvers. When the solver reports unsatisfiability, the formula is valid in the logic; when it reports satisfiability, the assignment supplies an explicit countermodel. The method is shown to work for the full Cn hierarchy of paraconsistent logics, where it improves on prior tools and supplies the first implementation, and it remains competitive for intuitionistic propositional logic and the fifteen normal modal logics. A reader would care because these logics already possess sound and complete RNmatrix semantics, yet those semantics had remained too cumbersome for routine computational use until the encoding made them directly executable.

Core claim

By representing the truth tables of an RNmatrix together with its elimination criteria as formulas in an SMT theory, the validity of a formula in the corresponding logic reduces to an SMT satisfiability query; unsatisfiability of the query establishes validity while a satisfying assignment directly yields a countermodel in the original RNmatrix.

What carries the argument

RNmatrix semantics together with their row-elimination criteria, encoded as SMT constraints whose satisfiability decides formula validity.

If this is right

  • Validity checking for formulas in the target logics reduces to an SMT satisfiability query.
  • Countermodels are extracted automatically from any satisfying assignment returned by the solver.
  • The procedure supplies the first implementation for the entire Cn hierarchy of paraconsistent logics.
  • The same encoding yields competitive performance on intuitionistic propositional logic and all fifteen normal modal logics of the modal cube.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding pattern could be reused for any other logic already known to possess an RNmatrix semantics.
  • Hybridizing the SMT encoding with additional theories supported by the same solvers may extend the method to quantified or first-order versions of these logics.
  • Performance advantages observed on paraconsistent logics suggest that SMT solvers can serve as a generic computational backend for many non-classical logics that previously lacked efficient implementations.

Load-bearing premise

The known sound and complete RNmatrix semantics for the target logics can be translated into SMT constraints without introducing incompleteness or prohibitive overhead.

What would settle it

A formula that the SMT prover declares valid but that possesses a countermodel under the original RNmatrix semantics, or a formula the prover declares invalid but that is valid according to the RNmatrix.

Figures

Figures reproduced from arXiv: 2605.01845 by Carlos Olarte, Elaine Pimentel, Renato R. Leme.

Figure 1
Figure 1. Figure 1: Fig. 1a shows the time taken by TRiNity for completing the 45 entries of Cn_propag for different logics Cn; Fig. 1b shows the number of subformulas for the instance i = 500 for the different families in the benchmarks for C1; Fig. 1c compares TRiNity vs gen2sat for the benchmarks on C1. Items below the diagonal are instances that TRiNity solved faster. For logic C1, we benchmark TRiNity against gen2sat wit… view at source ↗
Figure 2
Figure 2. Figure 2: Benchmarks for logic S4. On the left, the maximum number of instances solved in 1 minute view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims that by encoding Restricted Non-deterministic Matrices (RNmatrices) together with their row-elimination criteria as Satisfiability Modulo Theories (SMT) problems, off-the-shelf SMT solvers can be used to decide formula validity and generate countermodels for a range of non-classical logics. The approach is illustrated on paraconsistent logics (including the full Cn hierarchy, for which it supplies the first implementation and outperforms prior provers), intuitionistic propositional logic, and the fifteen normal modal logics of the modal cube, where the resulting general-purpose prover is reported to be competitive.

Significance. If the SMT encoding is shown to be faithful and the performance claims are backed by reproducible benchmarks, the work would supply the first practical, uniform decision procedure for the broad class of logics known to possess RNmatrix semantics. This fills a documented gap, since prior literature established soundness and completeness of RNmatrices but offered no efficient implementations. The use of an external, mature SMT solver is a pragmatic strength that could be extended to other semantic frameworks.

major comments (1)
  1. [SMT Encoding Section] The section presenting the SMT encoding (approximately §4) does not contain a formal theorem, reduction, or bisimulation argument establishing that unsatisfiability of the generated SMT instance is equivalent to non-validity under the original RNmatrix semantics. Because the row-filtering elimination criteria are translated into constraints on non-deterministic operations, an explicit equivalence proof is required to guarantee that the procedure inherits the known soundness and completeness of RNmatrices rather than introducing new sources of incompleteness or spurious countermodels.
minor comments (2)
  1. [Abstract] The abstract states that the prover 'outperforms the current state-of-the-art' for paraconsistent logics yet supplies no reference to the specific benchmark tables, instance sets, or timeout values used; these metrics should be cited already in the abstract for immediate assessment.
  2. [Preliminaries] Notation for the RNmatrix elimination criteria (e.g., the precise definition of 'valid rows') is introduced without a running example that shows both the original matrix and its SMT encoding side-by-side; adding such an example would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need for an explicit equivalence result between the SMT encoding and the original RNmatrix semantics. We agree this strengthens the presentation and will revise the manuscript to include it.

read point-by-point responses

  1. Referee: [SMT Encoding Section] The section presenting the SMT encoding (approximately §4) does not contain a formal theorem, reduction, or bisimulation argument establishing that unsatisfiability of the generated SMT instance is equivalent to non-validity under the original RNmatrix semantics. Because the row-filtering elimination criteria are translated into constraints on non-deterministic operations, an explicit equivalence proof is required to guarantee that the procedure inherits the known soundness and completeness of RNmatrices rather than introducing new sources of incompleteness or spurious countermodels.

    Authors: We agree that an explicit theorem is desirable. In the revised version we will add Theorem 4.1 in §4: for any RNmatrix M and formula φ, φ is valid in M if and only if the SMT instance generated by the encoding is unsatisfiable. The proof proceeds by structural induction on φ, showing that each SMT constraint directly mirrors the definition of RNmatrix evaluation (including the row-elimination filter translated as additional clauses on the non-deterministic choice variables). Because the translation is a faithful syntactic rendering of the semantic clauses, no new restrictions are introduced and the known soundness/completeness of RNmatrices is inherited. A short reduction argument will also be supplied to make the correspondence transparent. revision: yes

Circularity Check

0 steps flagged

No circularity: SMT encoding applies external solver to independently defined RNmatrix semantics

full rationale

The paper encodes pre-existing RNmatrix semantics (with their row-elimination criteria) as SMT constraints to decide validity. Soundness and completeness of the semantics are taken from prior literature on RNmatrices for paraconsistent, intuitionistic and modal logics; the encoding step is presented as a faithful translation that leverages an off-the-shelf SMT solver rather than deriving any result from fitted parameters or self-referential definitions. No equation or claim in the abstract or described method reduces a performance result or validity decision to a construction that is tautological with its inputs. The reported outperformance is empirical benchmarking against external tools, not a self-derived prediction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on the prior soundness and completeness results for RNmatrix semantics (cited but not re-derived) and on the standard semantics of SMT solvers; no new free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption RNmatrix semantics are sound and complete for the target logics
    Invoked when the paper states that the framework enables sound and complete semantics for paraconsistent, intuitionistic, and modal logics.
  • standard math SMT solvers correctly decide the satisfiability of the generated constraints
    Implicit reliance on the correctness of off-the-shelf SMT technology.

pith-pipeline@v0.9.0 · 5491 in / 1287 out tokens · 45919 ms · 2026-05-09T16:30:52.549210+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 16 canonical work pages

  1. [1]

    In Werner Horn, editor:ECAI 2000, Proceedings of the 14th European Conference on Artificial Intelligence, Berlin, Germany, August 20-25, 2000, IOS Press, pp

    Carlos Areces, Rosella Gennari, Juan Heguiabehere & Maarten de Rijke (2000):Tree-based Heuristics in Modal Theorem Proving. In Werner Horn, editor:ECAI 2000, Proceedings of the 14th European Conference on Artificial Intelligence, Berlin, Germany, August 20-25, 2000, IOS Press, pp. 199–203

    2000

  2. [2]

    Arnon Avron (2007):Non-deterministic semantics for logics with a consistency operator.Int. J. Approx. Reason.45(2), pp. 271–287, doi:10.1016/J.IJAR.2006.06.011

    work page doi:10.1016/j.ijar.2006.06.011 2007

  3. [3]

    Arnon Avron & Iddo Lev (2005):Non-deterministic Multiple-valued Structures.J. Log. Comput.15(3), pp. 241–261, doi:10.1093/logcom/exi001

    work page doi:10.1093/logcom/exi001 2005

  4. [4]

    Arnon Avron & Anna Zamansky (2011):Non-Deterministic Semantics for Logical Systems, pp. 227–304. Springer Netherlands, Dordrecht, doi:10.1007/978-94-007-0479-4_4

    work page doi:10.1007/978-94-007-0479-4_4 2011

  5. [5]

    Arnon Avron & Yoni Zohar (2019):Rexpansions of Nondeterministic matrices and their Applications in nonclassical Logics.Rev. Symb. Log.12(1), pp. 173–200, doi:10.1017/S1755020318000321

    work page doi:10.1017/s1755020318000321 2019

  6. [6]

    Coniglio (2016):Some Extensions of mbC

    Walter Carnielli & Marcelo E. Coniglio (2016):Some Extensions of mbC. In:Paraconsistent Logic: Con- sistency, Contradiction and Negation,Logic, Epistemology, and the Unity of Science40, Springer, Cham, doi:10.1007/978-3-319-33205-5_3

    work page doi:10.1007/978-3-319-33205-5_3 2016

  7. [7]

    Agata Ciabattoni, Ori Lahav, Lara Spendier & Anna Zamansky (2014):Taming Paraconsistent (and Other) Logics: An Algorithmic Approach.ACM Trans. Comput. Log.16(1), pp. 5:1–5:23, doi:10.1145/2661636

    work page doi:10.1145/2661636 2014

  8. [8]

    In:Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp

    Koen Claessen & Dan Rosén (2015):SAT Modulo Intuitionistic Implications. In:Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, pp. 622–637

    2015

  9. [9]

    601–642, doi:10.1007/S11225-021-09972-Z

    Marcelo E Coniglio & Guilherme V Toledo (2022):Two Decision Procedures for da Costa’s Cn Logics Based on Restricted Nmatrix Semantics.Studia Logica110(3), pp. 601–642, doi:10.1007/S11225-021-09972-Z

    work page doi:10.1007/s11225-021-09972-z 2022

  10. [10]

    Newton C. A. da Costa (1974):On the theory of inconsistent formal systems.Notre Dame J. Formal Log. 15(4), pp. 497–510, doi:10.1305/NDJFL/1093891487. Renato R. Leme & Carlos Olarte & Elaine Pimentel17

    work page doi:10.1305/ndjfl/1093891487 1974

  11. [11]

    Inconsistent formal systems

    Newton C. A. da Costa (1993):Sistemas formais inconsistentes. Ph.D. thesis, Universidade Federal do Paraná, Curitiba, Brazil. Habilitation thesis (1963). Republished by Editora UFPR, 1993. Portuguese title; English: “Inconsistent formal systems”

    1993

  12. [12]

    Newton CA Da Costa & Elias H Alves (1977):A semantical analysis of the calculi Cn.Notre Dame Journal of Formal Logic18(4), pp. 621–630

    1977

  13. [13]

    Itala M Loffredo D’Ottaviano & Milton Augustinis De Castro (2006):Analytical tableaux for da costa’s hierarchy of paraconsistent logics.Electronic Notes in Theoretical Computer Science143, pp. 27–44

    2006

  14. [14]

    James Dugundji (1940):Note on a Property of Matrices for Lewis and Langford’s Calculi of Propositions.J. Symb. Log.5(4), pp. 150–151, doi:10.2307/2268175

    work page doi:10.2307/2268175 1940

  15. [15]

    Dawson, Stephen C

    Solomon Feferman, John W. Dawson, Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay & Jean van Heijenoort (1986):Kurt Gödel: Collected Works. Vol. 1: Publications 1929-1936. Oxford University Press

    1986

  16. [16]

    In:Interna- tional Conference on Automated Deduction, Springer, pp

    Camillo Fiorentini (2021):Efficient SAT-based proof search in intuitionistic propositional logic. In:Interna- tional Conference on Automated Deduction, Springer, pp. 217–233

    2021

  17. [17]

    Kurt Gödel (1932):Zum intuitionistischen aussagenkalkül.Anzeiger der Akademie der Wissenschaften in Wien69, pp. 65–66. English translation as ‘On the intuitionistic propositional calculus’. In [15], pp. 223, 225

    1932

  18. [18]

    Lukas Grätz (2022):Truth tables for modal logics T and S4, by using three-valued non-deterministic level semantics.J. Log. Comput.32(1), pp. 129–157, doi:10.1093/logcom/exab068

    work page doi:10.1093/logcom/exab068 2022

  19. [19]

    Kearns (1981):Modal Semantics without Possible Worlds.J

    John T. Kearns (1981):Modal Semantics without Possible Worlds.J. Symb. Log.46(1), pp. 77–86, doi:10.2307/2273259

    work page doi:10.2307/2273259 1981

  20. [20]

    Ori Lahav & Yoni Zohar (2022):Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. In Jasmin Blanchette, Laura Kovács & Dirk Pattinson, editors:Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings,Lecture Notes in Computer Science13385, Springer, pp. 468–485, doi:...

    work page doi:10.1007/978-3-031-10769-6_28 2022

  21. [21]

    Renato Leme, Carlos Olarte, Elaine Pimentel & Marcelo Esteban Coniglio (2025):The Modal Cube Re- visited: Semantics Without Worlds. In Gian Luca Pozzato & Tarmo Uustalu, editors:Automated Reasoning with Analytic Tableaux and Related Methods - 34th International Conference, TABLEAUX 2025, Reykjavik, Iceland, September 27-29, 2025, Proceedings, Lecture Note...

    work page doi:10.1007/978-3-032-06085-3_10 2025

  22. [22]

    Leme, Marcelo E

    Renato R. Leme, Marcelo E. Coniglio & Bruno Lopes (2025):A New Decision Method for Intuition- istic Logic by 3-Valued Non-Deterministic Truth-Tables.The Journal of Symbolic Logic, pp. 1–36, doi:10.1017/jsl.2025.10174

    work page doi:10.1017/jsl.2025.10174 2025

  23. [23]

    Leme & Carlos Olarte (2026):TRiNity: A Matrix-Based Theorem Prover

    Renato R. Leme & Carlos Olarte (2026):TRiNity: A Matrix-Based Theorem Prover. Available at https: //depot.lipn.univ-paris13.fr/provers/trinity

    2026

  24. [24]

    In:Proceedings of the 3rd Brazilian Conference on Mathematical Logic, Sociedade Brasileira de Lógica, pp

    Andréa Loparic & Elias Alves (1980):The semantics of the systems Cn of da Costa. In:Proceedings of the 3rd Brazilian Conference on Mathematical Logic, Sociedade Brasileira de Lógica, pp. 161–172

    1980

  25. [25]

    Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini & Clare Dixon (2022):Local Reductions for the Modal Cube. In Jasmin Christian Blanchette, Laura Kovács & Dirk Pattinson, editors:Proceedings of the Interna- tional Joint Conference on Automated Reasoning (IJCAR 2022),Lecture Notes in Computer Science13385, Springer, Cham, doi:10.1007/978-3-031-10769-6_29

    work page doi:10.1007/978-3-031-10769-6_29 2022

  26. [26]

    In:Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelli- gence, IJCAI-17, pp

    Cláudia Nalon, Ullrich Hustadt & Clare Dixon (2017):KSP: A Resolution-based Prover for Multimodal K, Abridged Report. In:Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelli- gence, IJCAI-17, pp. 4919–4923, doi:10.24963/ijcai.2017/694. Available at https://doi.org/10.24963/ijcai. 2017/694

    work page doi:10.24963/ijcai.2017/694 2017

  27. [27]

    Adolfo Neto, Celso AA Kaestner & Marcelo Finger (2009):Towards an Efficient Prover for the C1 Paracon- sistent Logic.Electronic Notes in Theoretical Computer Science256, pp. 87–102. 18Efficient Decision Procedures for RNmatrix Semantics

    2009

  28. [28]

    In:IFIP International Conference on Artificial Intelligence in Theory and Practice, Springer, pp

    Adolfo Gustavo Serra Seca Neto & Marcelo Finger (2006):Effective Prover for Minimal Inconsistency Logic. In:IFIP International Conference on Artificial Intelligence in Theory and Practice, Springer, pp. 465–474

    2006

  29. [29]

    Brunetto Piochi (1978):Matrici adequate per calcoli generali predicativi.Bolletino della Unione Matemat- ica Italiana A15, pp. 66–76

    1978

  30. [30]

    Brunetto Piochi (1983):Logical matrices and non-structural consequence operators.Studia Logica42(1), pp. 33–42

    1983

  31. [31]

    In:European Workshop on Logics in Artificial Intelligence, Springer, pp

    Dmitry Tishkovsky, Renate A Schmidt & Mohammad Khodadadi (2012):The tableau prover generator MetTeL2. In:European Workshop on Logics in Artificial Intelligence, Springer, pp. 492–495

    2012