pith. sign in

arxiv: 2212.09570 · v3 · submitted 2022-12-19 · 💻 cs.LO · cs.AI

Solving Quantified Modal Logic Problems by Translation to Classical Logics

Alexander Steen , Geoff Sutcliffe , Christoph Benzm\"uller This is my paper

Pith reviewed 2026-05-24 10:10 UTC · model grok-4.3

classification 💻 cs.LO cs.AI
keywords quantified modal logicautomated theorem provingembedding translationQMLTPclassical ATP systemsmodal logic semantics
0
0 comments X

The pith

Translating quantified modal logic problems into classical first-order and higher-order logic allows standard automated theorem provers to solve them reliably.

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

The paper evaluates an embedding approach that converts problems from the QMLTP library of first-order modal logic into typed first-order and higher-order logic in TPTP format. These translated problems are then solved using classical ATP systems and model finders, with results compared against native modal logic ATP systems. The evaluation shows the embeddings succeed with state-of-the-art classical backends, that first-order and higher-order versions perform similarly, that native modal systems match the embedding method for proving theorems but are outperformed for disproving conjectures, and that the embedding method covers a broader set of modal logics.

Core claim

The embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners. The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered.

What carries the argument

The embedding translations that map quantified modal logic problems into typed first-order and higher-order classical logic in TPTP syntax.

If this is right

  • The embedding process succeeds when paired with state-of-the-art classical ATP systems.
  • First-order and higher-order embeddings yield similar performance.
  • Native modal ATP systems perform comparably to the embedding approach on theorem proving tasks.
  • The embedding approach outperforms native modal systems on conjecture disproving tasks.
  • The embedding approach applies to a wider range of modal logics than the native systems tested.

Where Pith is reading between the lines

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

  • For tasks that emphasize finding counterexamples, the embedding route may be the more practical choice over native modal systems.
  • The close performance of first-order and higher-order embeddings suggests that problem difficulty in this domain is not strongly tied to the classical logic level chosen.

Load-bearing premise

The embedding translations correctly preserve the semantics of the modal logics for the QMLTP problems so that classical ATP systems determine theoremhood or non-theoremhood without distortion.

What would settle it

A QMLTP problem for which the embedding approach returns a different theorem/non-theorem result than the problem's actual status under the modal logic semantics.

Figures

Figures reproduced from arXiv: 2212.09570 by Alexander Steen, Christoph Benzm\"uller, Geoff Sutcliffe.

Figure 1
Figure 1. Figure 1: Non-classical connective examples tff(pigs_fly_decl,type, pigs_fly: $o ). tff(flying_pigs_impossible,axiom, ~ {$possible} @ (pigs_fly) ). tff(alice_knows_pigs_dont_fly,axiom, {$knows(#alice)} @ (~ pigs_fly) ). tff(something_is_necessary,axiom, ? [P: $o] : {$necessary} @ (P) ). tff(a_decl,type, a: $i ). tff(f_decl,type, f: $i > $o ). tff(reasonable,conjecture, ( ! [X: $i] : ( {$box} @ (f(X)) ) => ( {$box} @… view at source ↗
Figure 2
Figure 2. Figure 2: Embedding process (picture taken from [38]) [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
read the original abstract

This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-order and higher-order logic in the TPTP language using an embedding approach, and solved using first-order resp. higher-order logic ATP systems and model finders. Additionally, the results from native modal logic ATP systems are considered, and compared with the results from the embedding approach. The findings are that the embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners, The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered.

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 / 0 minor

Summary. The paper evaluates ATP performance on the QMLTP library of quantified modal logic problems. Problems are translated via embeddings to typed first-order logic and higher-order logic in TPTP syntax and solved with classical ATP systems and model finders; results are compared against native modal ATP systems. The central claims are that the embedding process is reliable with state-of-the-art backends, that first-order and higher-order embeddings perform similarly, that native modal systems are comparable to embedded classical systems on theorem proving but outperformed on disproving, and that embeddings handle a wider range of modal logics than the native systems considered.

Significance. If the embeddings preserve semantics, the work shows that mature classical ATP technology can be applied to quantified modal logics with competitive or superior performance on disproofs and broader modal axiom coverage than current native modal provers. The direct empirical comparison on the public QMLTP benchmark supplies concrete data on the practical utility of the embedding route.

major comments (1)
  1. [Abstract / evaluation] Abstract and evaluation results: the claim that 'the embedding process is reliable and successful' rests on empirical success rates with ATP backends, but no independent verification (e.g., model comparison with a native modal model finder, hand-checked small cases, or explicit checks on domain semantics, rigidity, or accessibility encoding) is reported to confirm that the translations preserve theoremhood/non-theoremhood for the QMLTP problems.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and constructive comment. We respond point by point below.

read point-by-point responses

  1. Referee: [Abstract / evaluation] Abstract and evaluation results: the claim that 'the embedding process is reliable and successful' rests on empirical success rates with ATP backends, but no independent verification (e.g., model comparison with a native modal model finder, hand-checked small cases, or explicit checks on domain semantics, rigidity, or accessibility encoding) is reported to confirm that the translations preserve theoremhood/non-theoremhood for the QMLTP problems.

    Authors: The embeddings employed are those introduced and proven sound and complete in our prior publications on semantic embeddings for quantified modal logics (with respect to standard Kripke semantics, including varying domains, rigid designators, and accessibility relations). The present manuscript is an empirical performance study of these established translations when used with classical ATP systems, not a re-verification of the translations themselves. The reliability claim rests on the combination of the prior formal results and the observed high success rates together with consistency against native modal systems on theorem-proving tasks. We nevertheless agree that the manuscript would benefit from an explicit reminder of the semantic-preservation results. In the revised version we will add a short subsection that summarises the relevant soundness theorems from the cited embedding papers and notes that the QMLTP results exhibited no unexpected discrepancies with known modal behaviour. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical benchmark evaluation on external QMLTP library

full rationale

The paper reports an empirical comparison of ATP performance on the public QMLTP benchmark after applying embedding translations to classical logics. No equations, predictions, or central claims reduce by construction to fitted parameters, self-definitions, or self-citation chains. Results are obtained by direct execution against independent native modal systems and public problem sets; semantic preservation is an external correctness assumption rather than a self-referential step in any derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The evaluation rests on the assumption that prior embedding translations are semantics-preserving; no free parameters or invented entities are introduced.

axioms (1)
  • domain assumption Embedding translations preserve the semantics of the modal logics considered for the QMLTP problems.
    This premise is required for the reliability and performance claims to hold.

pith-pipeline@v0.9.0 · 5690 in / 1306 out tokens · 27081 ms · 2026-05-24T10:10:04.309286+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

56 extracted references · 56 canonical work pages

  1. [1]

    P.B. Andrews. General Models and Extensionality. Journal of Symbolic Logic, 37(2):395–397, 1972

    work page 1972

  2. [2]

    R. Barcan. A Functional Calculus of First Order Based on Strict Implica- tion. Journal of Symbolic Logic, 11:1–16, 1946. 18

    work page 1946

  3. [3]

    Benzmüller

    C. Benzmüller. Universal (Meta-)Logical Reasoning: Recent Successes. Science of Computer Programming, 172:48–62, 2019

    work page 2019

  4. [4]

    Benzmüller, C.E

    C. Benzmüller, C.E. Brown, and M. Kohlhase. Higher-order Semantics and Extensionality. Journal of Symbolic Logic, 69(4):1027–1088, 2004

    work page 2004

  5. [5]

    Benzmüller and D

    C. Benzmüller and D. Miller. Automation of Higher-Order Logic. In D. Gabbay, J. Siekmann, and J. Woods, editors,Handbook of the History of Logic, volume 9 - Computational Logic, pages 215–254. North Holland, Elsevier, 2014

    work page 2014

  6. [6]

    Benzmüller, J

    C. Benzmüller, J. Otten, and T. Raths. Implementing and Evaluat- ing Provers for First-order Modal Logics. In L. De Raedt, C. Bessiere, D. Dubois, P. Doherty, P. Frasconi, F. Heintz, and P. Lucas, editors,Pro- ceedings of the 20th European Conference on Artificial Intelligence, Fron- tiers in Artificial Intelligence and Applications, pages 163–168. IOS Pr...

    work page 2012

  7. [7]

    Benzmüller and L

    C. Benzmüller and L. Paulson. Quantified Multimodal Logics in Simple Type Theory. Logica Universalis, 7(1):7–20, 2013

    work page 2013

  8. [8]

    Benzmüller and T

    C. Benzmüller and T. Raths. HOL Based First-order Modal Logic Provers. In K. McMillan, A. Middeldorp, and A. Voronkov, editors, Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, number 8312 in Lecture Notes in Computer Science, pages 127–136. Springer-Verlag, 2013

    work page 2013

  9. [9]

    Benzmüller and B

    C. Benzmüller and B. Woltzenlogel Paleo. The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics. In S. Kamb- hampati, editor,Proceedings of the 25th International Joint Conference on Artificial Intelligence, pages 936–942. AAAI Press, 2016

    work page 2016

  10. [10]

    Bhayat and G

    A. Bhayat and G. Reger. A Combinator-based Superposition Calculus for Higher-Order Logic. In N. Peltier and V. Sofronie-Stokkermans, edi- tors, Proceedings of the 10th International Joint Conference on Automated Reasoning, number 12166 in Lecture Notes in Artificial Intelligence, pages 278–296, 2020

    work page 2020

  11. [11]

    Blackburn, M

    P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001

    work page 2001

  12. [12]

    Blackburn, J

    P. Blackburn, J. van Benthem, and F. Wolther.Handbook of Modal Logic. Number 3 in Studies in Logic and Practical Reasoning. Elsevier Science, 2006

    work page 2006

  13. [13]

    Blanchette and T

    J. Blanchette and T. Nipkow. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In M. Kaufmann and L. Paulson, editors,Proceedings of the 1st International Conference on Interactive Theorem Proving, number 6172 in Lecture Notes in Computer Science, pages 131–146. Springer-Verlag, 2010. 19

    work page 2010

  14. [14]

    Braüner and S

    T. Braüner and S. Ghilardi. First-order modal logic. In P. Blackburn, J. van Benthem, and F. Wolter, editors,Handbook of Modal Logic, pages 549–620. Elsevier B.V., 2007

    work page 2007

  15. [15]

    A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5:56–68, 1940

    work page 1940

  16. [16]

    Fariñas del Cerro, D

    L. Fariñas del Cerro, D. Fauthoux, O. Gasquet, A. Herzig, D. Longin, and F. Massacci. LoTREC: The Generic Tableau Prover for Modal and Descrip- tion Logics. In R. Gore, A. Leitsch, and T. Nipkow, editors,Proceedings of the International Joint Conference on Automated Reasoning, number 2083 in Lecture Notes in Artificial Intelligence, pages 453–458. Springe...

    work page 2083

  17. [17]

    Fitting and R

    M. Fitting and R. Mendelsohn.First-Order Modal Logic. Kluwer, 1998

    work page 1998

  18. [18]

    Frege.Grundgesetze der Arithmetik

    F. Frege.Grundgesetze der Arithmetik. Jena, 1893,1903

    work page 1903

  19. [19]

    J. Garson. Modal Logic. In E. Zalta, editor, Stanford Encyclopedia of Philosophy. Stanford University, 2018

    work page 2018

  20. [20]

    Gibbons and N

    J. Gibbons and N. Wu. Folding Domain-specific Languages: Deep and Shallow Embeddings (Functional Pearl). In J. Jeuring and M. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pages 339–347. ACM Press, 2014

    work page 2014

  21. [21]

    Gleißner, A

    T. Gleißner, A. Steen, and C. Benzmüller. Theorem Provers for Every Normal Modal Logic. In T. Eiter and D. Sands, editors,Proceedings of the 21st International Conference on Logic for Programming, Artificial In- telligence, and Reasoning, number 46 in EPiC Series in Computing, pages 14–30. EasyChair Publications, 2017

    work page 2017

  22. [22]

    Gordon and T

    M. Gordon and T. Melham. Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993

    work page 1993

  23. [23]

    Harrison

    J. Harrison. HOL Light: A Tutorial Introduction. In M. Srivas and A. Camilleri, editors, Proceedings of the 1st International Conference on Formal Methods in Computer-Aided Design, number 1166 in Lecture Notes in Computer Science, pages 265–269. Springer-Verlag, 1996

    work page 1996

  24. [24]

    L. Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic, 15(2):81–91, 1950

    work page 1950

  25. [25]

    MSPASS:ModalReasoningbyTranslationand First-Order Resolution

    U.HustadtandR.Schmidt. MSPASS:ModalReasoningbyTranslationand First-Order Resolution. In R. Dyckhoff, editor,Proceedings of the Inter- national Conference on Automated Reasoning with Analytic Tableaux and Related Methods, number 1847 in Lecture Notes in Artificial Intelligence, pages 67–71. Springer-Verlag, 2000. 20

    work page 2000

  26. [26]

    S. Kripke. Semantical Considerations on Modal Logic.Acta Philosophica Fennica, 16:83–94, 1963

    work page 1963

  27. [27]

    Nalon, U

    C. Nalon, U. Hustadt, and C. Dixon. KSP: Architecture, Refinements, Strategies and Experiments.Journal of Automated Reasoning, 64(3):461– 484, 2020

    work page 2020

  28. [28]

    Nipkow, L

    T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assis- tant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science. Springer-Verlag, 2002

    work page 2002

  29. [29]

    H.J. Ohlbach. Semantics Based Translation Methods for Modal Logics. Journal of Logic and Computation, 1(5):691–746, 1991

    work page 1991

  30. [30]

    J. Otten. MleanCoP: A Connection Prover for First-Order Modal Logic. In S. Demri, D. Kapur, and C. Weidenbach, editors,Proceedings of the 7th International Joint Conference on Automated Reasoning, number 8562 in Lecture Notes in Artificial Intelligence, pages 269–276, 2014

    work page 2014

  31. [31]

    J. Otten. The nanoCoP 2.0 Connection Provers for Classical, Intuition- istic and Modal Logics. In A. Das and S. Negri, editors,Proceedings of the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, number 12842 in Lecture Notes in Artificial Intelligence, pages 236–249. Springer-Verlag, 2021

    work page 2021

  32. [32]

    Otten and G

    J. Otten and G. Sutcliffe. Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi. In B. Konev, R. Schmidt, and S. Schulz, editors,Proceedings of the Workshop on Practical Aspects of Automated Reasoning, 5th International Joint Conference on Automated Reasoning, pages 90–100, 2010

    work page 2010

  33. [33]

    S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Com- bining Specification, Proof Checking, and Model Checking. In R. Alur and T.A. Henzinger, editors,Computer-Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 411–414. Springer-Verlag, 1996

    work page 1996

  34. [34]

    Papacchini, C

    F. Papacchini, C. Nalon, U. Hustadt, and C. Dixon. Efficient Local Reduc- tions to Basic Modal Logic. In A. Platzer and G. Sutcliffe, editors,Proceed- ings of the 28th International Conference on Automated Deduction, number 12699 in Lecture Notes in Computer Science, pages 76–92. Springer-Verlag, 2021

    work page 2021

  35. [35]

    Raths and J

    T. Raths and J. Otten. The QMLTP Problem Library for First-Order Modal Logics. In B. Gramlich, D. Miller, and U. Sattler, editors,Proceed- ings of the 6th International Joint Conference on Automated Reasoning, number 7364 in Lecture Notes in Artificial Intelligence, pages 454–461. Springer-Verlag, 2012. 21

    work page 2012

  36. [36]

    Schulz, S

    S. Schulz, S. Cruanes, and P. Vukmirović. Faster, Higher, Stronger: E 2.3. In P. Fontaine, editor,Proceedings of the 27th International Conference on Automated Deduction, number 11716 in Lecture Notes in Computer Science, pages 495–507. Springer-Verlag, 2019

    work page 2019

  37. [37]

    Siekmann, C

    J. Siekmann, C. Benzmüller, and S. Autexier. Computer Supported Math- ematics with OMEGA.Journal of Applied Logic, 4(4):533–559, 2006

    work page 2006

  38. [38]

    A. Steen. An extensible logic embedding tool for lightweight non-classical reasoning (short paper). In B. Konev, C. Schon, and A. Steen, editors,Pro- ceedings of the 8th Workshop on Practical Aspects of Automated Reasoning, number 3201 in CEUR Workshop Proceedings, page Online, 2022

    work page 2022

  39. [39]

    A. Steen. logic-embedding v1.8.4, 2024. DOI: 10.5281/zenodo.10819185

    work page doi:10.5281/zenodo.10819185 2024

  40. [40]

    Steen and C

    A. Steen and C. Benzmüller. The Higher-Order Prover Leo-III. In D. Galmiche, S. Schulz, and R. Sebastiani, editors,Proceedings of the 8th International Joint Conference on Automated Reasoning, number 10900 in Lecture Notes in Artificial Intelligence, pages 108–116, 2018

    work page 2018

  41. [41]

    Solv- ing Quantified Modal Logic Problems by Translation to Classical Logics

    A. Steen, G. Sutcliffe, and C. Benzmüller. Supplemental material to “Solv- ing Quantified Modal Logic Problems by Translation to Classical Logics”,

    work page

  42. [42]

    DOI: 10.5281/zenodo.10802221

    work page doi:10.5281/zenodo.10802221

  43. [43]

    Steen, G

    A. Steen, G. Sutcliffe, T. Scholl, and C. Benzmüller. Solving Modal Logic Problems by Translation to Higher-order Logic. In A. Herzig, J. Luo, and P. Pardo, editors,Proceedings of the 5th International Conference on Logic and Argumentation, number 14156 in Lecture Notes in Computer Science, pages 25–43. Springer, 2023. (Best paper award)

    work page 2023

  44. [44]

    Stump, G

    A. Stump, G. Sutcliffe, and C. Tinelli. StarExec: a Cross-Community In- frastructure for Logic Solving. In S. Demri, D. Kapur, and C. Weidenbach, editors, Proceedings of the 7th International Joint Conference on Auto- mated Reasoning, number 8562 in Lecture Notes in Artificial Intelligence, pages 367–373, 2014

    work page 2014

  45. [45]

    Sutcliffe

    G. Sutcliffe. TPTP, TSTP, CASC, etc. In V. Diekert, M. Volkov, and A. Voronkov, editors,Proceedings of the 2nd International Symposium on Computer Science in Russia, number 4649 in Lecture Notes in Computer Science, pages 6–22. Springer-Verlag, 2007

    work page 2007

  46. [46]

    Sutcliffe

    G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017

    work page 2017

  47. [47]

    Sutcliffe

    G. Sutcliffe. The Logic Languages of the TPTP World.Logic Journal of the IGPL, 31(6):1153–1169, 2023. 22

    work page 2023

  48. [48]

    Sutcliffe and C

    G. Sutcliffe and C. Benzmüller. Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure.Journal of Formalized Reason- ing, 3(1):1–27, 2010

    work page 2010

  49. [49]

    Sutcliffe, J

    G. Sutcliffe, J. Zimmer, and S. Schulz. TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In W. Zhang and V. Sorge, editors, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Sys- tems, number 112 in Frontiers in Artificial Intelligence and Applications, pages 201–215. IOS Press, 2004

    work page 2004

  50. [50]

    Thion, S

    V. Thion, S. Cerrito, and M. Cialdea Mayer. A General Theorem Prover for Quantified Modal Logics. In U. Egly and C. Fermüller, editors,Proceedings of the 11th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, number 2381 in Lecture Notes in Computer Science, pages 266–280. Springer, 2002

    work page 2002

  51. [51]

    Tishkovsky, R

    D. Tishkovsky, R. Schmidt, and M. Khodadadi. The Tableau Prover Gen- erator MetTeL2. In L. Fariñas del Cerro, A. Herzig, and J. Mengin, editors, Proceedings of the 13th European conference on Logics in Artificial Intelli- gence, number 7519 in Lecture Notes in Computer Science, pages 492–495. Springer, 2012

    work page 2012

  52. [52]

    van Ditmarsch, J

    H. van Ditmarsch, J. Halpern, W. van der Hoek, and B. Kooi.Handbook of Epistemic Logic. College Publications, 2015

    work page 2015

  53. [53]

    Vukmirović, A

    P. Vukmirović, A. Bentkamp, J. Blanchette, S. Cruanes, V. Nummelin, and S. Tourret. Making Higher-order Superposition Work. In A. Platzer and G. Sutcliffe, editors,Proceedings of the 28th International Conference on Automated Deduction, number 12699 in Lecture Notes in Computer Science, pages 415–432. Springer-Verlag, 2021. Author information

    work page 2021

  54. [54]

    Alexander Steen University of Greifswald, Germany alexander.steen@uni-greifswald.de ORCID: 0000-0001-8781-9462

    work page

  55. [55]

    Geoff Sutcliffe University of Miami, USA geoff@cs.miami.edu ORCID: 0000-0001-9120-3927

    work page

  56. [56]

    Christoph Benzmüller University of Bamberg and FU Berlin, Germany christoph.benzmueller@uni-bamberg.de ORCID: 0000-0002-3392-30935 23

    work page