Pith. sign in

REVIEW 2 major objections 6 minor 61 references

Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?

T0 review · 2 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Language models mostly fail to follow the modal-logic semantics they are explicitly given, but high reasoning mode can restore that sensitivity.

desk verdict Clean paired design nails the direct-prompt failure; the reasoning-mode jump is real data on an opaque knob, not yet a mechanism claim. read the letter →

arxiv 2608.05097 v1 pith:BTWE5ZWC submitted 2026-08-05 cs.CL

Réemi Andrieu , Damien Sileo This is my paper
classification cs.CL MSC 03B4568T50
keywords modallogiclanguagemodelssemanticadaptationKripkeframesquantifiedreasoningmodebenchmarkdesignframeanddomainconditions
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper asks whether language models follow the modal-logic semantics they are told to use, rather than silently falling back on a familiar default logic. It builds paired reasoning problems with identical premises and conjecture but different frame or domain conditions, so the same formula must be accepted under one specification and rejected under another. On a balanced core where a condition-only strategy would score 50 percent, four of five tested models score below that baseline under direct prompting. Only Claude Sonnet 5 exceeds it, while enabling a high reasoning mode lifts DeepSeek V4 Flash from 4.4 percent to 88.1 percent strict pair accuracy on unchanged prompts. The paper concludes that semantic control is a separate ability from modal knowledge, and that fixed-semantics benchmarks can overstate robustness.

What carries the argument

The central object is the paired two-specification problem: one formula, possibly with premises, and one conjecture, evaluated under two semantics that differ in a single frame property (seriality, reflexivity, symmetry, transitivity) or domain rule (no appearance, no disappearance), with an automated-reasoning oracle verifying opposite labels. The balanced non-nested core crosses the conditions so that each condition appears equally often with each label, making 50 percent strict pair accuracy the ceiling for a strategy that reads only the stated semantics without reading the formula. Strict pair accuracy, which requires both judgments in a pair to be correct, is the metric that separates following the specification from applying a fixed default logic.

What would settle it

Rerun the 160-pair balanced core on a fresh model endpoint under direct prompting: if a model scores substantially above 50 percent strict pair accuracy with high within-condition balanced accuracy, the claim that direct-prompt models mostly ignore the stated semantics fails for that model. As a second check, if the 88.1 percent high-reasoning result disappears when the same prompt is served through a non-reasoning route with an equally large output-token budget, the reasoning effect is a format artifact rather than inference-time computation.

Watch

Extended reading notes

Core claim

In the paper's own terms, success requires tracking the stated semantics rather than applying one fixed modal logic, and current language models largely fail at this when prompted directly. Keeping the formula fixed and changing only one declared frame property or domain rule makes the oracle-verified label flip between the two specifications; on the balanced non-nested core, direct strict-pair accuracy ranges from 2.5 to 25.0 percent for four of five models, below the 50 percent condition-only baseline, while Claude Sonnet 5 scores 65.0 percent. With unchanged prompts and a high reasoning setting, DeepSeek V4 Flash reaches 88.1 percent strict pair accuracy, showing that inference-time computation can restore sensitivity to the stipulated semantics even though the intermediate derivations remain unreliable. When frame conditions are omitted, models exhibit coherent affinities with familiar default modal systems—the weakest normal logic K or the reflexive logic T—but these defaults do not predict their explicit errors.

Load-bearing premise

The load-bearing premise is that the oracle labels are correct, meaning the automated translation and proving pipeline plus the independent Kripke checker faithfully implement the intended quantified modal semantics, and that API reasoning-mode settings measure a genuine computation change rather than a prompt-format artifact.

Editorial extensions

If this is right

  • Benchmarks that fix a single intended semantics can overstate a model's reasoning ability, since a model may do well by exploiting a default logic instead of the stated rules.
  • Following a stated specification is not guaranteed by having coherent modal knowledge: a model can know a default logic yet fail to suspend it when a local rule demands it.
  • Inference-time computation, such as high reasoning effort, can change whether a model reacts to a semantic intervention at all, even when no reasoning language is added to the prompt.
  • Representation choices (named conditions, relational definitions, formal syntax) change which errors appear, but no single format reliably restores semantic control.
  • Underspecified prompts are filled in by models with different default logics, mostly the weakest normal logic K or the reflexive logic T, so agreement across models does not imply correctness under any particular semantics.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If this result generalizes, applications in deontic or legal reasoning should treat a model's answer as valid only under the explicitly declared frame and domain conditions, and should test sensitivity to those conditions rather than single-answer accuracy.
  • A testable extension is to use answer-change rate as a primary diagnostic: on paired problems, a model that never changes its answer when the semantics flips has zero semantic control, regardless of its one-sided accuracy.
  • The reasoning-mode effect predicts that increasing inference-time computation should raise specification-sensitivity for other models as well, but only if the computation can revise the default logic rather than merely elaborate it; this could be probed by comparing prompted rationales with hidden reasoning settings that leave the prompt unchanged.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper introduces a paired-diagnostic evaluation for whether LLMs follow explicitly stipulated modal-logic semantics. It constructs problems with identical premises and conjecture but different frame or domain conditions, uses automated theorem provers (Vampire, Leo-III) and an independent Kripke countermodel checker to assign opposite labels, and builds a balanced 160-pair core that removes condition-only shortcuts. Five recent LLMs are evaluated under direct prompting and, for some models, under API reasoning modes. The main findings are that four of five models score below the 50% condition-only baseline on the balanced core under direct prompting, and that enabling a high reasoning mode raises DeepSeek V4 Flash from 4.4% to 88.1% on unchanged prompts. The paper also reports semantic-affinity and representation-sensitivity pilots and releases formulas, oracle artifacts, countermodels, and responses.

Significance. If the main claims hold, the paper makes a valuable methodological contribution: it separates whether a model follows a stated semantics from whether it applies a fixed default modal logic, and it provides a clean, balanced experimental design with a principled baseline. Strengths include the paired construction that fixes lexical content and formula difficulty, the balanced core that forces formula-sensitive judgment, oracle labels backed by ATP artifacts and independent finite countermodel checks for invalid sides, transparent handling of malformed outputs, Wilson intervals and bootstrap resampling, and the release of code and data. The direct-prompt failure result is well supported within its scope. The inference-mode result, however, is less secure because it depends on a single proprietary API configuration and one sample per side, which the paper itself acknowledges.

major comments (2)
  1. [Section 6, Table 5, Appendix C, and Limitations] The headline claim that reasoning mode restores semantic sensitivity (DeepSeek V4 Flash rising from 4.4% to 88.1% on the balanced core) is load-bearing for the abstract and Section 6, but it rests on a single proprietary API configuration (reasoning.effort: high), one sample per side, and an unversioned endpoint. The Limitations section states that API reasoning levels are neither transparent nor calibrated across vendors, and Appendix C notes that each API condition uses one sample. The GPT-4.1 prompted-rationale pilot in Table 14 is not a mechanism control because it changes the prompt rather than the inference procedure, and its +24 point gain does not reproduce the +80 point gain. I request either a transparent inference-time intervention (e.g., an open-weights model with controlled chain-of-thought decoding, or multiple runs with reported variance) before claiming that inference-time computation restores semantic control, or an explicit downgrade of this result to exploratory.
  2. [Section 4 and Table 12] In the balanced core, 24 of 160 valid sides have only a single-prover proof (Leo-III) with no independent verification, while all invalid sides receive independent Kripke-countermodel checks. Since the balanced-core results are the basis for the central below-baseline finding, a small number of label errors in those 24 pairs could affect the comparison with the 50% baseline. I ask for dual-prover agreement for those sides, an independent model-based check of the negated conjecture, or a sensitivity analysis that excludes single-prover pairs from Table 2. The paper's limitation about labels inheriting LET embedding and prover assumptions is honest, but a quantitative sensitivity check would strengthen the central claim.
minor comments (6)
  1. [Section 2] The phrase 'QMLTP, the interoperable non-classical TPTP format' is imprecise: QMLTP is a problem library, while the TPTP infrastructure for non-classical logics is described in Steen and Sutcliffe (2025). Please reword to avoid conflating the library with the format.
  2. [Figure 1] The notation 'p→23p' in the frame-core panel is confusing; if it is intended as p → 2 3 p (necessarily possibly p), please insert spacing or parentheses and define the symbols in the caption.
  3. [Table 2] The column headers 'B↔S4↑' and 'Cum.↔Dec.↑' are not explained; define what the arrow denotes (e.g., 'contrast direction' or 'axis') in the caption or remove the arrows.
  4. [Table 14 caption] The phrase 'Parse is the enhanced-condition pair parse rate' is unclear; state explicitly that this is the pair-level parse rate in the reasoning-mode or rationale condition, and define 'enhanced-condition'.
  5. [References] The reference to 'Kovács and V oronkov' contains an unwanted space; it should read 'Voronkov'.
  6. [Appendix C] The sentence 'The DeepSeek condition retains the direct prompt and sends reasoning.effort: high with a 2,048-token maximum output tokens' has a grammatical error; it should be 'with maximum output tokens set to 2,048'.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the central results rest on externally verified oracle labels and a balanced test design, not on fitted parameters or load-bearing self-citation.

full rationale

The paper's derivation chain is self-contained against external benchmarks. Problem pairs are generated from fixed formula schemas and semantic conditions; oracle labels come from Vampire and Leo-III through the LET embedding, with invalid balanced-core sides additionally checked by an independent Kripke evaluator. These labels are produced without consulting model outputs, so the opposite labels within each pair are not constructed from the models' behavior. The balanced-core design explicitly removes the condition-only shortcut by balancing each semantic condition across both labels, so the 50% baseline is a genuine null strategy rather than a disguised fit. Model accuracy is then measured directly on unchanged prompts. The reasoning-mode comparison changes an API setting while holding prompts fixed; although the paper acknowledges that API reasoning levels are neither transparent nor calibrated across vendors and that each condition uses one sample, this is an external-validity limitation, not circularity. The semantic-affinity fits are post hoc descriptions of behavior and are not used to derive the headline failure or the reasoning-mode result. The one self-citation (Sileo and Lernould, 2023) appears only as an example of fixed-semantics modal evaluation in related work and does not carry any load-bearing argument. The paper also explicitly flags that labels inherit LET embedding and prover assumptions, which is an honest statement of oracle assumptions rather than a circular reuse of the conclusion. Overall, no claimed prediction reduces by construction to its input, and no load-bearing step depends on an unverified self-citation.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central claim depends on standard modal semantics, actualist quantification, and the correctness of the LET/ATP oracle pipeline. No free parameters are fitted to the data. No new entities are postulated.

assumptions (6)
  • standard math Standard Kripke frame semantics for K, D, T, B, S4, and S5, with serial, reflexive, symmetric, and transitive frames as defined in Section 3.
    Provides the target semantics that oracle labels evaluate and prompts describe.
  • domain assumption Actualist quantification over nonempty per-world domains with variable assignments retaining the same object across worlds (Appendix A).
    Required for the first-order domain contrasts; a different semantics could change labels.
  • domain assumption The LET embedding plus Vampire and Leo-III correctly decide the quantified modal validity problems, so every retained oracle label matches the intended semantics.
    The paper states labels inherit LET and prover assumptions and rejects conflicts and unresolved sides.
  • domain assumption The independent Kripke evaluator correctly verifies finite countermodels for all invalid sides of the balanced core.
    The authors report a two- or three-world countermodel checked by this evaluator for each invalid balanced-core side.
  • domain assumption The deterministic controlled-English renderer expresses the formal semantics without adding unintended cues.
    Prompts spell out rules but withhold system names; the renderer is deterministic.
  • domain assumption API reasoning settings act as a within-model capability intervention rather than a degenerate response-format change.
    Reasoning-mode runs use unchanged prompts and temperature zero, but the paper notes API reasoning levels are not transparent.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?." pith.science (2026). https://pith.science/paper/BTWE5ZWC

@misc{pith2026260805097,
  author       = {Pith},
  title        = {Pith review of: Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BTWE5ZWC}},
  note         = {Machine review of arXiv:2608.05097}
}
read the original abstract

Reasoning about necessity and possibility depends on assumptions about accessibility between worlds and about which objects exist at each one. The same inference may therefore hold under one modal system and fail under another. Evaluating language models on such problems requires testing whether their judgments follow the stated semantics rather than a familiar logic. We construct paired modal problems with identical premises and conjecture but different frame or domain conditions; automated reasoning verifies opposite labels. A balanced core prevents the semantic condition alone from revealing the answer. On this core, four of five recent models perform below the condition-only baseline under direct prompting. Yet enabling reasoning mode raises DeepSeek V4 Flash from 4.4% to 88.1% on unchanged prompts. Following stipulated modal semantics thus depends strongly on inference mode as well as model identity. When frame conditions are omitted, models often agree but fit different familiar logics best. We release the formulas, oracle artifacts, countermodels, and responses.

Figures

Figures reproduced from arXiv: 2608.05097 by the authors.

Figure 1
Figure 1. The two balanced-core contrasts. The problem formula is fixed within each pair; only one explicit rule [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

61 extracted references · 53 canonical work pages

  1. [1]

    Lasha Abzianidze, Joost Zwarts, and Yoad Winter. 2023. https://aclanthology.org/2023.naloma-1.2/ SpaceNLI : Evaluating the consistency of predicting inferences in space . In Proceedings of the 4th Natural Logic Meets Machine Learning Workshop, pages 12--24. Association for Computational Linguistics

    work page 2023

  2. [2]

    Ruth C. Barcan. 1946. https://doi.org/10.2307/2269159 A functional calculus of first order based on strict implication . Journal of Symbolic Logic, 11(1):1--16

    work page doi:10.2307/2269159 1946

  3. [3]

    Mendelsohn

    Melvin Fitting and Richard L. Mendelsohn. 1998. First-Order Modal Logic. Kluwer Academic Publishers

    work page 1998

  4. [4]

    Liu, Phoebe Mulcaire, Qiang Ning, and 7 others

    Matt Gardner, Yoav Artzi, Victoria Basmov, Jonathan Berant, Ben Bogin, Sihao Chen, Pradeep Dasigi, Dheeru Dua, Yanai Elazar, Ananth Gottumukkala, Nitish Gupta, Hannaneh Hajishirzi, Gabriel Ilharco, Daniel Khashabi, Kevin Lin, Jiangming Liu, Nelson F. Liu, Phoebe Mulcaire, Qiang Ning, and 7 others. 2020. https://doi.org/10.18653/v1/2020.findings-emnlp.117 ...

    doi:10.18653/v1/2020.findings-emnlp.117 2020

  5. [5]

    Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alex Wardle-Solano, Hannah Szabo, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, and 16 others. 2022. FOLIO : Natural language reasoning with first-order logic. In Proceed...

    work page 2022

  6. [6]

    Holliday, Matthew Mandelkern, and Cedegao E

    Wesley H. Holliday, Matthew Mandelkern, and Cedegao E. Zhang. 2024. https://arxiv.org/abs/2401.17169 Conditional and modal reasoning in large language models . Preprint, arXiv:2401.17169

    arXiv 2024

  7. [7]

    Laura Kov \'a cs and Andrei Voronkov. 2013. https://doi.org/10.1007/978-3-642-39799-8_1 First-order theorem proving and Vampire . In Computer Aided Verification, volume 8044 of Lecture Notes in Computer Science, pages 1--35. Springer

    doi:10.1007/978-3-642-39799-8_1 2013

  8. [8]

    Saul A. Kripke. 1963. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83--94

    work page 1963

Show all 61 references
  1. [9]

    Xianglong Li, Yu Liu, Botao Zhang, Mingjing Jiang, and Yunfei Chen. 2025. https://api.semanticscholar.org/CorpusID:280409061 Modallogicbench: Unveiling modal logic reasoning abilities of large language models . In International Conference on Intelligent Computing

    2025

  2. [10]

    Mihir Parmar, Nisarg Patel, Neeraj Varshney, Mutsumi Nakamura, Man Luo, Santosh Mashetty, Arindam Mitra, and Chitta Baral. 2024. LogicBench : Towards systematic evaluation of logical reasoning ability of large language models. In Proceedings of the 62nd Annual Meeting of the A...

    2024

  3. [11]

    Thomas Raths and Jens Otten. 2012. https://doi.org/10.1007/978-3-642-31365-3_35 The QMLTP problem library for first-order modal logics . In Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 454--461. Springer

    2012 doi

  4. [12]

    Damien Sileo and Antoine Lernould. 2023. https://doi.org/10.18653/v1/2023.findings-emnlp.303 M ind G ames: Targeting theory of mind in large language models with dynamic epistemic modal logic . In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 457...

    2023 doi

  5. [13]

    Alexander Steen. 2022. An extensible logic embedding tool for lightweight non-classical reasoning. In Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning, volume 3201 of CEUR Workshop Proceedings

    2022

  6. [14]

    Alexander Steen and Christoph Benzm \"u ller. 2021. Extensional higher-order paramodulation in Leo-III . Journal of Automated Reasoning, 65:775--807

    2021

  7. [15]

    Alexander Steen and Geoff Sutcliffe. 2025. https://doi.org/10.48550/arXiv.2508.09318 TPTP world infrastructure for non-classical logics . Preprint, arXiv:2508.09318

    2025 doi arXiv

  8. [16]

    Alexander Steen, Geoff Sutcliffe, and Christoph Benzm \"u ller. 2024. Solving quantified modal logic problems by translation to classical logics. Journal of Automated Reasoning. Also available as arXiv:2212.09570

    2024 arXiv

  9. [17]

    Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. ProofWriter : Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621--3634

    2021

  10. [18]

    Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. 2021. https://doi.org/10.18653/v1/2021.emnlp-main.303 Diagnosing the first-order logical reasoning ability through L ogic NLI . In Proceedings of the 2021 Conference on Empirical Methods in Natural Lan...

    2021 doi

  11. [19]

    Yixuan Wang and Freda Shi. 2025. https://doi.org/10.18653/v1/2025.acl-long.824 Logical forms complement probability in understanding language model (and human) performance . In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: L...

    2025 doi

  12. [20]

    2018 , eprint=

    The Higher-Order Prover Leo-III (Extended Version) , author=. 2018 , eprint=

    2018

  13. [21]

    Multi- L ogi E val: Towards Evaluating Multi-Step Logical Reasoning Ability of Large Language Models

    Patel, Nisarg and Kulkarni, Mohith and Parmar, Mihir and Budhiraja, Aashna and Nakamura, Mutsumi and Varshney, Neeraj and Baral, Chitta. Multi- L ogi E val: Towards Evaluating Multi-Step Logical Reasoning Ability of Large Language Models. Proceedings of the 2024 Conference on ...

    2024 doi

  14. [22]

    L ogic A sker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models

    Wan, Yuxuan and Wang, Wenxuan and Yang, Yiliu and Yuan, Youliang and Huang, Jen-tse and He, Pinjia and Jiao, Wenxiang and Lyu, Michael. L ogic A sker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models. Proceedings of the 2024 Conference on Empiric...

    2024 doi

  15. [23]

    Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative Grammars

    Sileo, Damien. Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative Grammars. Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing. 2024. doi:10.18653/v1/2024.emnlp-main.301

    2024 doi

  16. [24]

    2023 , pages =

    Sileo, Damien and Lernould, Antoine , booktitle =. 2023 , pages =

    2023

  17. [25]

    2024 , eprint=

    Conditional and Modal Reasoning in Large Language Models , author=. 2024 , eprint=

    2024

  18. [26]

    Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , year =

    Logical forms complement probability in understanding language model (and human) performance , author =. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) , year =

  19. [27]

    ArXiv , year=

    Empowering LLMs with Logical Reasoning: A Comprehensive Survey , author=. ArXiv , year=

  20. [28]

    ArXiv , year=

    AutoLogi: Automated Generation of Logic Puzzles for Evaluating Reasoning Abilities of Large Language Models , author=. ArXiv , year=

  21. [29]

    ArXiv , year=

    OneEval: Benchmarking LLM Knowledge-intensive Reasoning over Diverse Knowledge Bases , author=. ArXiv , year=

  22. [30]

    2025 , eprint=

    Normative Reasoning in Large Language Models: A Comparative Benchmark from Logical and Modal Perspectives , author=. 2025 , eprint=

    2025

  23. [31]

    2026 , eprint=

    Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning , author=. 2026 , eprint=

    2026

  24. [32]

    2026 , eprint=

    Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training , author=. 2026 , eprint=

    2026

  25. [33]

    2026 , eprint=

    DeonticBench: A Benchmark for Reasoning over Rules , author=. 2026 , eprint=

    2026

  26. [34]

    International Conference on Intelligent Computing , year=

    ModalLogicBench: Unveiling Modal Logic Reasoning Abilities of Large Language Models , author=. International Conference on Intelligent Computing , year=

  27. [35]

    Procedia Computer Science , year=

    LogiCue: Targeted Prompting for Improved Modal and Conditional Reasoning in Large Language Models , author=. Procedia Computer Science , year=

  28. [36]

    TechRxiv , volume =

    Sophia Richter and Mareike Gerhardt and Jan Muller and Lukas Bauer , title =. TechRxiv , volume =. 2025 , doi =. https://www.techrxiv.org/doi/pdf/10.36227/techrxiv.176581130.09718203/v1 , abstract =

    2025

  29. [37]

    Mathematics , VOLUME =

    Liang, Baoyu and Wang, Yuchen and Tong, Chao , TITLE =. Mathematics , VOLUME =. 2025 , NUMBER =

    2025

  30. [38]

    1980 , publisher=

    Naming and Necessity , author=. 1980 , publisher=

    1980

  31. [39]

    , title =

    Barcan, Ruth C. , title =. Journal of Symbolic Logic , year =

  32. [40]

    , title =

    Kripke, Saul A. , title =. Acta Philosophica Fennica , year =

  33. [41]

    2001 , series =

    Blackburn, Patrick and de Rijke, Maarten and Venema, Yde , title =. 2001 , series =

    2001

  34. [42]

    Hughes, G. E. and Cresswell, M. J. , title =

  35. [43]

    , title =

    Fitting, Melvin and Mendelsohn, Richard L. , title =

  36. [44]

    Journal of Automated Reasoning , year =

    Sutcliffe, Geoff , title =. Journal of Automated Reasoning , year =

  37. [45]

    Logic for Programming, Artificial Intelligence, and Reasoning , year =

    Sutcliffe, Geoff , title =. Logic for Programming, Artificial Intelligence, and Reasoning , year =

  38. [46]

    Automated Reasoning in Non-classical Logics in the

    Steen, Alexander and Fuenmayor, David and Glei. Automated Reasoning in Non-classical Logics in the. 2022 , eprint =

    2022

  39. [47]

    Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning , year =

    Steen, Alexander , title =. Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning , year =

  40. [48]

    Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logic , journal =

    Benzm. Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logic , journal =. 2011 , volume =

    2011

  41. [49]

    Quantified Multimodal Logics in Simple Type Theory , journal =

    Benzm. Quantified Multimodal Logics in Simple Type Theory , journal =. 2013 , volume =

    2013

  42. [50]

    Extensional Higher-Order Paramodulation in

    Steen, Alexander and Benzm. Extensional Higher-Order Paramodulation in. Journal of Automated Reasoning , year =

  43. [51]

    First-Order Theorem Proving and

    Kov. First-Order Theorem Proving and. Computer Aided Verification , year =

  44. [52]

    Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021 , year =

    Tafjord, Oyvind and Dalvi, Bhavana and Clark, Peter , title =. Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021 , year =

    2021

  45. [53]

    Han, Simeng and Schoelkopf, Hailey and Zhao, Yilun and Qi, Zhenting and Riddell, Martin and Zhou, Wenfei and Coady, James and Peng, David and Qiao, Yujie and Benson, Luke and Sun, Lucy and Wardle-Solano, Alex and Szabo, Hannah and Zubova, Ekaterina and Burtell, Matthew and Fan...

    2022

  46. [54]

    Advances in Neural Information Processing Systems , year =

    Saparov, Abulhair and Pang, Richard Yuanzhe and Padmakumar, Vishakh and Joshi, Nitish and Kazemi, Seyed Mehran and Kim, Najoung and He, He , title =. Advances in Neural Information Processing Systems , year =

  47. [55]

    Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics , year =

    Parmar, Mihir and Patel, Nisarg and Varshney, Neeraj and Nakamura, Mutsumi and Luo, Man and Mashetty, Santosh and Mitra, Arindam and Baral, Chitta , title =. Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics , year =

  48. [56]

    Proceedings of the 4th Natural Logic Meets Machine Learning Workshop , year =

    Abzianidze, Lasha and Zwarts, Joost and Winter, Yoad , title =. Proceedings of the 4th Natural Logic Meets Machine Learning Workshop , year =

  49. [57]

    Findings of the Association for Computational Linguistics: EMNLP 2020 , year =

    Evaluating Models' Local Decision Boundaries via Contrast Sets , author =. Findings of the Association for Computational Linguistics: EMNLP 2020 , year =

    2020

  50. [58]

    Diagnosing the First-Order Logical Reasoning Ability Through

    Tian, Jidong and Li, Yitian and Chen, Wenqing and Xiao, Liqiang and He, Hao and Jin, Yaohui , booktitle =. Diagnosing the First-Order Logical Reasoning Ability Through. 2021 , pages =

    2021

  51. [59]

    Automated Reasoning , year =

    Raths, Thomas and Otten, Jens , title =. Automated Reasoning , year =

  52. [60]

    Solving Quantified Modal Logic Problems by Translation to Classical Logics , journal =

    Steen, Alexander and Sutcliffe, Geoff and Benzm. Solving Quantified Modal Logic Problems by Translation to Classical Logics , journal =. 2024 , note =

    2024

  53. [61]

    2025 , eprint =

    Steen, Alexander and Sutcliffe, Geoff , title =. 2025 , eprint =

    2025

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.