Pith. sign in

REVIEW 2 major objections 3 minor 1 cited by

TPTP World Infrastructure for Non-classical Logics

T0 review · 2 major / 3 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read This paper claims that the TPTP World, since release v9.0.0, provides a complete infrastructure for automated theorem proving in non-classical logics, demonstrated through a quantified normal multi-modal logic workflow.

desk verdict An infrastructure overview whose value depends on the semantic correctness of the released non-classical TPTP artifacts—worth peer review, but I can't fully verify it from the abstract alone. read the letter →

arxiv 2508.09318 v1 pith:237A5RTX submitted 2025-08-12 cs.LO cs.AI

Alexander Steen , Geoff Sutcliffe This is my paper · ORCID
classification cs.LOcs.AI MSC 03B4503B3568T15
keywords TPTPnon-classicallogicmodalautomatedtheoremprovingbenchmarkinfrastructurequantifiedmulti-modalproblemlibraryATPsystems
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

The paper describes the TPTP World's extension, starting with release v9.0.0, to non-classical logics. It aims to establish that the established benchmark-and-tool infrastructure for classical automated theorem proving now covers non-classical logics through a dedicated language extension, a problem-and-solution corpus, and tool support. A detailed treatment of quantified normal multi-modal logic shows how users can write problems, run provers, and interpret results inside one unified framework. A sympathetic reader would take this as the non-classical ATP community gaining a standardized, citable evaluation ecosystem in the style of the classical TPTP.

What carries the argument

The central object is the TPTP World: the established collection of syntax standards, benchmark problems, and tools for automated theorem proving. The mechanism that carries this paper's claim is the non-classical language extension added in v9.0.0 — a syntax layer that lets formulas of modal and other non-classical logics be expressed in TPTP syntax — together with the associated problem and solution records and the tool support that links them to provers. The paper's detailed workflow for quantified normal multi-modal logic is the concrete demonstration of that mechanism.

What would settle it

Run two independently implemented provers that accept the TPTP v9.0.0 non-classical language against the published non-classical problem set and compare their outputs with the recorded solutions. If any problem recorded as a theorem is refuted by a countermodel under the documented Kripke semantics, or if independent provers disagree systematically, the infrastructure's correctness claim fails.

Watch

Extended reading notes

Core claim

The paper's central claim is that TPTP World release v9.0.0 and later provides comprehensive infrastructure for automated theorem proving in non-classical logics. The infrastructure consists of three connected parts: a non-classical language extension that lets formulas from modal and other non-classical logics be written in TPTP syntax; a library of non-classical problems with recorded solutions; and tool support that connects these problems to running provers. The paper gives a detailed account of using this infrastructure for quantified normal multi-modal logic, treating that case as the concrete demonstration of the general design.

Load-bearing premise

The load-bearing premise is that the TPTP v9.0.0+ non-classical artifacts — the language encoding, the problem statements, the stored solutions, and the tool support — are real and semantically correct under the intended Kripke-style semantics; the abstract asserts their existence but offers no machine-checked or independently verified evidence for that correctness.

Editorial extensions

If this is right

  • Researchers can state non-classical problems in a common TPTP syntax instead of per-system formats, making benchmarks portable.
  • The v9.0.0+ problem library gives non-classical prover developers a shared corpus with recorded solutions, so different systems can be compared directly.
  • The quantified normal multi-modal logic workflow can serve as a template for applying the same infrastructure to other non-classical logics.
  • Published problem and solution records make non-classical ATP experiments reproducible and citable, matching the classical TPTP model.
  • Existing TPTP-compatible tooling can be reused for non-classical problems rather than built from scratch.

Reading between the lines

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

  • If the encodings and solution records are semantically faithful, the non-classical ATP field could see the same benchmark-driven progress the classical TPTP enabled, because shared test sets make prover strengths and weaknesses visible.
  • The language extension appears logic-parametric; extending it to intuitionistic, deontic, or substructural logics would mostly require defining the intended semantics, not inventing new infrastructure.
  • A natural validation experiment, not reported in the abstract, is to run independent provers over the published problems; agreement with the stored solutions would support the claim, while disagreement would expose a semantic gap.
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 / 3 minor

Summary. The paper claims that, since TPTP release v9.0.0, the TPTP World provides comprehensive infrastructure for automated theorem proving in non-classical logics: a non-classical language extension, a catalog of problems and solutions, and tool support, with a detailed workflow for quantified normal multi-modal logic. The text available for review is the abstract only; no body, appendices, or supplementary release materials were supplied for inspection.

Significance. If the claims hold, this is a valuable contribution: it would give the non-classical ATP community a standardized, citable benchmark ecosystem of the kind that has been crucial for classical TPTP. Because the artifacts are publicly released, the claims are independently checkable in principle, and the paper is descriptive rather than circular. The value depends on the semantic correctness and usability of the released infrastructure, which the abstract asserts but does not evidence.

major comments (2)
  1. [Full text / availability] The reviewable manuscript consists solely of the abstract; the full text is empty in the provided record. The paper's central claim is that TPTP v9.0.0+ provides correct and comprehensive non-classical ATP infrastructure. That claim is load-bearing and cannot be verified from the abstract. No solution records, semantic definitions, conformance tests, or independent-prover agreement are visible. This is an evidentiary gap, not a demonstrated error, but it prevents a positive assessment. If the full text contains validation, it was not available to me.
  2. [Abstract] The abstract's claim of 'comprehensive' infrastructure is underspecified. It does not state which non-classical logics are covered, what semantics are used for the non-classical connectives and quantifiers, or how the correctness of problems and solutions is established. For a benchmark infrastructure, these are not optional details: the entire value rests on the intended Kripke-style semantics being unambiguous and correctly implemented in both the problem encodings and the tool support.
minor comments (3)
  1. [Abstract] The abstract would benefit from persistent identifiers (URL/DOI) for the TPTP release and for the non-classical language specification, so that readers and reviewers can locate the artifact.
  2. [Abstract] The phrase 'non-classical logics' is broad. A short enumeration (e.g., quantified modal logic, intuitionistic logic, substructural logics) would clarify scope and give the reader a concrete sense of what 'comprehensive' means.
  3. [Abstract] The paper describes 'tool support' but no evaluation of its reliability. A sentence reporting e.g. numbers of problems with machine-checked solutions or agreement between independent provers would substantially strengthen the claim.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper is an infrastructure overview with no fitted predictions or self-referential derivation chain.

full rationale

The available text is an abstract describing the TPTP World's non-classical logic infrastructure since release v9.0.0: a language extension, problems and solutions, and tool support, with a detailed example for quantified normal multi-modal logic. There is no derivation chain, no fitted parameter, no prediction, and no invoked uniqueness theorem. The claims are existential assertions about a publicly released artifact that can be checked independently against the TPTP distribution and external provers. Self-description of one's own infrastructure is not circular reasoning, and the fact that the authors are describing their own work is not itself a circularity. The strongest concern—that the released problems might not be semantically correct under Kripke semantics—is an evidentiary gap rather than a circular step: the paper does not define the target result in terms of the artifact, nor does it present an unsupported self-citation as the load-bearing justification. Since no specific reduction of a claimed result to its own inputs can be exhibited from the available text, the circularity score is 0.

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

The paper's claims are descriptive claims about an existing artifact, so the ledger is short. No free parameters exist because nothing is fitted to data. The load-bearing premises are that the non-classical language extension has a well-defined, sound semantics, and that the publicly released TPTP artifacts match the description with correct benchmark solutions. No new theoretical entities are introduced; the non-classical language extension is an engineering artifact that stands or falls with the released system it describes.

assumptions (2)
  • domain assumption The non-classical TPTP language extension has a well-defined and sound semantics for quantified normal multi-modal logic.
    The abstract asserts language support and a usage walkthrough for quantified normal multi-modal logic, but it provides no statement of the semantic framework (for example, Kripke semantics with a specified interaction between quantifiers and modal operators) or of any validation of that semantics.
  • domain assumption The public TPTP v9.0.0+ release contains the described problems, solutions, and tools, and the solution records are correct.
    The overview's central value depends on the released artifact matching the description. The abstract gives no evidence such as machine-checked solutions or agreement of independent provers.

how reviews work

0 comments
Cite this review

Pith. "Pith review of TPTP World Infrastructure for Non-classical Logics." pith.science (2026). https://pith.science/paper/237A5RTX

@misc{pith2026250809318,
  author       = {Pith},
  title        = {Pith review of: TPTP World Infrastructure for Non-classical Logics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/237A5RTX}},
  note         = {Machine review of arXiv:2508.09318}
}
read the original abstract

The TPTP World is the well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP World supports a range of classical logics, and since release v9.0.0 has supported non-classical logics. This paper provides a self-contained comprehensive overview of the TPTP World infrastructure for ATP in non-classical logics: the non-classical language extension, problems and solutions, and tool support. A detailed description of use of the infrastructure for quantified normal multi-modal logic is given.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

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

    cs.CL 2026-08 conditional novelty 7.0 of 10

    Most language models ignore stipulated modal semantics under direct prompting, but reasoning mode can restore sensitivity on a balanced paired benchmark.

Reference graph

Works this paper leans on

108 extracted references · 79 canonical work pages · cited by 1 Pith paper

  1. [1]

    : The TPTP Problem Library and Associated Infrastructure

    barticle Sutcliffe , G. : The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0 . Journal of Automated Reasoning 59 ( 4 ), 483 -- 502 ( 2017 ) 10.1007/s10817-017-9407- barticle

    work page doi:10.1007/s10817-017-9407- 2017

  2. [2]

    : The TPTP World - Infrastructure for Automated Reasoning

    bchapter Sutcliffe , G. : The TPTP World - Infrastructure for Automated Reasoning . In: Clarke , E. , Voronkov , A. (eds.) Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning . Lecture Notes in Artificial Intelligence , pp. 1 -- 12 . Springer , ??? ( 2010 ) bchapter

    2010

  3. [3]

    , Schulz , S

    bchapter Sutcliffe , G. , Schulz , S. , Claessen , K. , Van Gelder , A. : Using the TPTP Language for Writing Derivations and Finite Interpretations . In: Furbach , U. , Shankar , N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning . Lecture Notes in Artificial Intelligence , pp. 67 -- 81 . Springer , ??? ( 2006 ) bchapter

    2006

  4. [4]

    : The SZS Ontologies for Automated Reasoning Software

    bchapter Sutcliffe , G. : The SZS Ontologies for Automated Reasoning Software . In: Sutcliffe , G. , Rudnicki , P. , Schmidt , R. , Konev , B. , Schulz , S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics . CEUR Workshop Proceedings , p...

    2008

  5. [5]

    : The CADE ATP System Competition - CASC

    barticle Sutcliffe , G. : The CADE ATP System Competition - CASC . AI Magazine 37 ( 2 ), 99 -- 101 ( 2016 ) barticle

    2016

  6. [6]

    u ller , C. : What are Non-classical Logics and Why Do We Need Them? An Extended Interview with Dov Gabbay and Leon van der Torre . K \

    barticle Steen , A. , Benzm \"u ller , C. : What are Non-classical Logics and Why Do We Need Them? An Extended Interview with Dov Gabbay and Leon van der Torre . K \"u nstliche Intelligenz ( 2024 ) 10.1007/s13218-023-00824- barticle

    work page doi:10.1007/s13218-023-00824- 2024

  7. [7]

    , Gliozzi , V

    barticle Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G. , Schwind , C. : Non-classical Logics for Knowledge Representation and Reasoning . Intelligenza Artificiale 5 ( 1 ), 127 -- 131 ( 2011 ) barticle

    2011

  8. [8]

    , Achen , A

    botherref Liberman , A. , Achen , A. , Rendsvig , R. : Dynamic Term-modal Logics for First-order Epistemic Planning . Artificial Intelligence 286 (2020) 10.1016/j.artint.2020.10330 botherref

    work page arXiv 2020

Show all 108 references
  1. [9]

    , Lehnherr , D

    bchapter Cachin , C. , Lehnherr , D. , Studer , T. : Modal and Justification Logics for Multi-agent Systems . In: Herzig , A. , Luo , J. , Pardo , P. (eds.) Proceedings of the 5th International Conference on Logic and Argumentation . Lecture Notes in Computer Science , pp. 3 -...

    2023

  2. [10]

    , Parent , X

    barticle Benzm \"u ller , C. , Parent , X. , Torre , L. : Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support . Artificial Intelligence 287 , 103348 ( 2020 ) barticle

    2020

  3. [11]

    u ller , C. , Woltzenlogel Paleo , B. : The Inconsistency in G \

    bchapter Benzm \"u ller , C. , Woltzenlogel Paleo , B. : The Inconsistency in G \"o del's Ontological Argument: A Success Story for AI in Metaphysics . In: Kambhampati , S. (ed.) Proceedings of the 25th International Joint Conference on Artificial Intelligence , pp. 936 -- 942...

    2016

  4. [12]

    : Towards a Computational Semantics

    bchapter Benthem , J. : Towards a Computational Semantics . In: G \"a rdenfors , P. (ed.) Generalized Quantifiers . Studies in Linguistics and Philosophy , vol. 31 ( 1987 ). 10.1007/978-94-009-3381-1\_ bchapter

    1987 doi

  5. [13]

    : What 'must' and 'can' Must and Can Mean

    barticle Kratzer , A. : What 'must' and 'can' Must and Can Mean . Linguistics and Philosophy 1 , 337 -- 355 ( 1977 ) barticle

    1977

  6. [14]

    : A Methodology for Hardware Verification Based on Logic Simulation

    barticle Bryant , R. : A Methodology for Hardware Verification Based on Logic Simulation . Journal of the Association for Computing Machinery 38 ( 2 ), 299 -- 328 ( 1991 ) barticle

    1991

  7. [15]

    u ller , C. : TPTP and Beyond: Representation of Quantified Non-Classical Logics . In: Benzm \

    bchapter Wisniewski , M. , Steen , A. , Benzm \"u ller , C. : TPTP and Beyond: Representation of Quantified Non-Classical Logics . In: Benzm \"u ller , C. , Otten , J. (eds.) Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logic...

    2016

  8. [16]

    , Benthem , J

    bbook Blackburn , P. , Benthem , J. , Wolther , F. : Handbook of Modal Logic . Studies in Logic and Practical Reasoning , vol. 3 . Elsevier Science , ??? ( 2006 ) bbook

    2006

  9. [17]

    , Cate , B

    bchapter Areces , C. , Cate , B. : Hybrid Logics . In: Blackburn , P. , Benthem , J. , Wolter , F. (eds.) Handbook of Modal Logic . Studies in Logic and Practical Reasoning , pp. 821 -- 868 . North-Holland , ??? ( 2007 ) bchapter

    2007

  10. [18]

    , Steen , A

    bchapter Glei ner , T. , Steen , A. , Benzm \"u ller , C. : Theorem Provers for Every Normal Modal Logic . In: Eiter , T. , Sands , D. (eds.) Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning . EPiC Series in Comp...

    2017

  11. [19]

    , Steen , A

    bchapter Glei ner , T. , Steen , A. : The MET: The Art of Flexible Reasoning with Modalities . In: Benzm \"u ller , C. , Ricca , F. , Parent , X. , Roman , D. (eds.) Proceedings of the 2nd International Joint Conference on Rules and Reasoning . Lecture Notes in Computer Scienc...

    2018

  12. [20]

    : An extensible logic embedding tool for lightweight non-classical reasoning (short paper)

    bchapter Steen , A. : An extensible logic embedding tool for lightweight non-classical reasoning (short paper) . In: Konev , B. , Schon , C. , Steen , A. (eds.) Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning . CEUR Workshop Proceedings , p. ( 2022 ...

    2022

  13. [21]

    , Fuenmayor , D

    bchapter Steen , A. , Fuenmayor , D. , Glei ner , T. , Sutcliffe , G. , Benzm \"u ller , C. : Automated Reasoning in Non-classical Logics in the TPTP World . In: Konev , B. , Schon , C. , Steen , A. (eds.) Proceedings of the 8th Workshop on Practical Aspects of Automated Reaso...

    2022

  14. [22]

    , Sutcliffe , G

    bchapter Steen , A. , Sutcliffe , G. : TPTP World Infrastructure for Non-classical Logics . In: Nalon , C. , Steen , A. , Suda , M. (eds.) Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning . CEUR Workshop Proceedings , pp. 74 -- 90 ( 2024 ) bchapter

    2024

  15. [23]

    : An Introduction to Non-Classical Logic: From If to Is

    bbook Priest , G. : An Introduction to Non-Classical Logic: From If to Is . Cambridge University Press , ??? ( 2008 ) bbook

    2008

  16. [24]

    : The Blackwell Guide to Philosophical Logic

    bbook Goble , L. : The Blackwell Guide to Philosophical Logic . Wiley-Blackwell , ??? ( 2001 ) bbook

    2001

  17. [25]

    , Mendelsohn , R

    bbook Fitting , M. , Mendelsohn , R. : First-Order Modal Logic . Synthese Library , vol. 480 . Springer , ??? ( 2023 ) bbook

    2023

  18. [26]

    : Alethic Modal Logics and Semantics

    bchapter Schurz , G. : Alethic Modal Logics and Semantics . In: Jacquette , D. (ed.) A Companion to Philosophical Logic , pp. 442 -- 477 . Wiley , ??? ( 2006 ) bchapter

    2006

  19. [27]

    : Deontic Logic: Introductory and Systematic Readings

    bbook Hilpinen , R. : Deontic Logic: Introductory and Systematic Readings . D. Reidel , ??? ( 1971 ) bbook

    1971

  20. [28]

    , Halpern , J

    bbook Ditmarsch , H. , Halpern , J. , Hoek , W. , Kooi , B. : Handbook of Epistemic Logic . College Publications , ??? ( 2015 ) bbook

    2015

  21. [29]

    : Knowledge and Belief - An Introduction to the Logic of the Two Notions

    bbook Hintikka , J. : Knowledge and Belief - An Introduction to the Logic of the Two Notions . Texts in Philosophy . Cornell University Press , ??? ( 1962 ) bbook

    1962

  22. [30]

    , Rumberg , A

    bchapter Goranko , V. , Rumberg , A. : Temporal Logic . In: Zalta , E. (ed.) Stanford Encyclopedia of Philosophy . Stanford University , ??? ( 2022 ) bchapter

    2022

  23. [31]

    , Heuerding , A

    barticle Balsiger , P. , Heuerding , A. , Schwendimann , S. : A Benchmark Method for the Propositional Modal Logics K, KT, S4 . Journal of Automated Reasoning 24 ( 3 ), 297 -- 317 ( 2000 ) barticle

    2000

  24. [32]

    , Otten , J

    bchapter Raths , T. , Otten , J. : The QMLTP Problem Library for First-Order Modal Logics . In: Gramlich , B. , Miller , D. , Sattler , U. (eds.) Proceedings of the 6th International Joint Conference on Automated Reasoning . Lecture Notes in Artificial Intelligence , pp. 454 -...

    2012

  25. [33]

    , Otten , J

    bchapter Benzm \"u ller , C. , Otten , J. , Raths , T. : Implementing and Evaluating Provers for First-order Modal Logics . In: De Raedt , L. , Bessiere , C. , Dubois , D. , Doherty , P. , Frasconi , P. , Heintz , F. , Lucas , P. (eds.) Proceedings of the 20th European Confere...

    2012

  26. [34]

    a hnle , R. , Kerber , M. , Weidenbach , C. : Common Syntax of the DFG-Schwerpunktprogramm Deduction . Technical Report TR 10/96, Fakult \

    botherref H \"a hnle , R. , Kerber , M. , Weidenbach , C. : Common Syntax of the DFG-Schwerpunktprogramm Deduction . Technical Report TR 10/96, Fakult \"a t f \"u r Informatik, Univers \"a t Karlsruhe, Karlsruhe, Germany (1996) botherref

    1996

  27. [35]

    , Schmidt , R.A

    bchapter Hustadt , U. , Schmidt , R.A. : On Evaluating Decision Procedures for Modal Logics . In: M.E. , P. (ed.) Proceedings of the 15th International Joint Conference on Artificial Intelligence , pp. 202 -- 207 . Morgan Kaufmann , ??? ( 1997 ) bchapter

    1997

  28. [36]

    , Schmidt , R

    barticle Hustadt , U. , Schmidt , R. : Using Resolution for Testing Modal Satisfiability and Building Models . Journal of Automated Reasoning 28 ( 2 ), 205 -- 232 ( 2002 ) barticle

    2002

  29. [37]

    , Fikes , R.E

    botherref Genesereth , M.R. , Fikes , R.E. : Knowledge Interchange Format, Version 3.0 Reference Manual . Technical Report Logic-92-1, Computer Science Department, Stanford University (1992) botherref

    1992

  30. [38]

    ISO/IEC 24707:2018 (2018) botherref

    botherref ISO/IEC : Information technology - Common Logic (CL) - A Framework for a Family of Logic-based Languages . ISO/IEC 24707:2018 (2018) botherref

    2018

  31. [39]

    , Aranda , V

    bchapter Mazano , M. , Aranda , V. : Many-Sorted Logic . In: Zalta , E. , Nodelman , U. (eds.) Stanford Encyclopedia of Philosophy . Stanford University , ??? ( 2022 ) bchapter

    2022

  32. [40]

    , Kovacs , L

    bchapter Kotelnikov , E. , Kovacs , L. , Voronkov , A. : A First Class Boolean Sort in First-Order Theorem Proving and TPTP . In: Kerber , M. , Carette , J. , Kaliszyk , C. , Rabe , F. , Sorge , V. (eds.) Proceedings of the International Conference on Intelligent Computer Math...

    2015

  33. [41]

    : Completeness in the Theory of Types

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

    1950

  34. [42]

    : General Models and Extensionality

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

    1972

  35. [43]

    , Brown , C.E

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

    2004

  36. [44]

    : Normal Multimodal Logics: Automatic Deduction and Logic Programming Extensions

    botherref Baldoni , M. : Normal Multimodal Logics: Automatic Deduction and Logic Programming Extensions . PhD thesis, Universita degli studi di Torino, Torino, Italy (1998) botherref

    1998

  37. [45]

    : Modal Logic

    bchapter Garson , J. : Modal Logic . In: Zalta , E. (ed.) Stanford Encyclopedia of Philosophy . Stanford University , ??? ( 2018 ) bchapter

    2018

  38. [46]

    : Semantical Considerations on Modal Logic

    barticle Kripke , S. : Semantical Considerations on Modal Logic . Acta Philosophica Fennica 16 , 83 -- 94 ( 1963 ) barticle

    1963

  39. [47]

    : A Functional Calculus of First Order Based on Strict Implication

    barticle Barcan , R. : A Functional Calculus of First Order Based on Strict Implication . Journal of Symbolic Logic 11 , 1 -- 16 ( 1946 ) barticle

    1946

  40. [48]

    : Universal Grammar

    barticle Montague , R. : Universal Grammar . Theoria 36 ( 3 ), 373 -- 398 ( 1970 ) barticle

    1970

  41. [49]

    : The Proper Treatment of Quantification in Ordinary English

    bchapter Montague , R. : The Proper Treatment of Quantification in Ordinary English . In: Hintikka , K. , Moravcsik , J. , Suppes , P. (eds.) Approaches to Natural Language: Proceedings of the 1970 Stanford Workshop on Grammar and Semantics . Synthese Library, , pp. 221 -- 242...

    1970

  42. [50]

    : A General Interpreted Modal Calculus

    bbook Bressan , A. : A General Interpreted Modal Calculus . Yale University Press , ??? ( 1972 ) bbook

    1972

  43. [51]

    : Intensional and Higher-order Modal Logic

    bbook Gallin , D. : Intensional and Higher-order Modal Logic . North-Holland , ??? ( 1975 ) bbook

    1975

  44. [52]

    : Types, Tableaus, and G \"o del’s God

    bbook Fitting , M. : Types, Tableaus, and G \"o del’s God . Trends in Logic , vol. 12 . Springer , ??? ( 2002 ) bbook

    2002

  45. [53]

    , Suttner , C.B

    barticle Sutcliffe , G. , Suttner , C.B. : The TPTP Problem Library: CNF Release v1.2.1 . Journal of Automated Reasoning 21 ( 2 ), 177 -- 203 ( 1998 ) barticle

    1998

  46. [54]

    : The TPTP Problem Library and Associated Infrastructure

    barticle Sutcliffe , G. : The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0 . Journal of Automated Reasoning 43 ( 4 ), 337 -- 362 ( 2009 ) barticle

    2009

  47. [55]

    , Schulz , S

    bchapter Sutcliffe , G. , Schulz , S. , Claessen , K. , Baumgartner , P. : The TPTP Typed First-order Form with Arithmetic . In: Bj rner , N. , Voronkov , A. (eds.) Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasonin...

    2012

  48. [56]

    , Paskevich , A

    bchapter Blanchette , J. , Paskevich , A. : TFF1: The TPTP Typed First-order Form with Rank-1 Polymorphism . In: Bonacina , M.P. (ed.) Proceedings of the 24th International Conference on Automated Deduction . Lecture Notes in Artificial Intelligence , pp. 414 -- 420 . Springer...

    2013

  49. [57]

    , Kotelnikov , E

    bchapter Sutcliffe , G. , Kotelnikov , E. : TFX: The TPTP Extended Typed First-order Form . In: Konev , B. , Urban , J. , Schulz , S. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning . CEUR Workshop Proceedings , pp. 72 -- 87 ( 2018 ) bchapter

    2018

  50. [58]

    , Benzm \"u ller , C

    barticle Sutcliffe , G. , Benzm \"u ller , C. : Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure . Journal of Formalized Reasoning 3 ( 1 ), 1 -- 27 ( 2010 ) barticle

    2010

  51. [59]

    , Sutcliffe , G

    bchapter Kaliszyk , C. , Sutcliffe , G. , Rabe , F. : TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism . In: Fontaine , P. , Schulz , S. , Urban , J. (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning . CEUR Workshop Proceedings , ...

    2016

  52. [60]

    , Sutcliffe , G

    bchapter Van Gelder , A. , Sutcliffe , G. : Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation . In: Furbach , U. , Shankar , N. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning . Lecture Notes in Artificial In...

    2006

  53. [61]

    : What Is the Name of This Book? The Riddle of Dracula and Other Logical Puzzles

    bbook Smullyan , R.M. : What Is the Name of This Book? The Riddle of Dracula and Other Logical Puzzles . Prentice-Hall , ??? ( 1978 ) bbook

    1978

  54. [62]

    , Rott , P

    bchapter Egr \'e , P. , Rott , P. : The Logic of Conditionals . In: Zalta , E. (ed.) Stanford Encyclopedia of Philosophy . Stanford University , ??? ( 2021 ) bchapter

    2021

  55. [63]

    : Light Linear Logic

    barticle Girard , J.-Y. : Light Linear Logic . Information and Computation 143 ( 2 ), 175 -- 204 ( 1998 ) barticle

    1998

  56. [64]

    , Zimmer , J

    bchapter Sutcliffe , G. , Zimmer , J. , Schulz , S. : TSTP Data-Exchange Formats for Automated Theorem Proving Tools . In: Zhang , W. , Sorge , V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems . Frontiers in Artificial Intelligence and Appl...

    2004

  57. [65]

    , Thalman , L

    barticle Fitting , M. , Thalman , L. , Voronkov , A. : Term-Modal Logics . Studia Logica 69 ( 1 ), 133 -- 169 ( 2001 ) barticle

    2001

  58. [66]

    , Sano , K

    bchapter Sawasaki , T. , Sano , K. , Yamada , T. : Term-Sequence-Modal Logics . In: Blackburn , P. , Lorini , E. , Guo , M. (eds.) Proceedings of the 7th International Workshop on Logic, Rationality and Interaction . Lecture Notes in Computer Science , pp. 244 -- 258 . Springe...

    2019

  59. [67]

    , Kozen , D

    bchapter Harel , D. , Kozen , D. , Tiuryn , J. : Dynamic Logic . In: Gabbay , D. , Guenthner , F. (eds.) Handbook of Philosophical Logic vol. 4 , pp. 99 -- 217 . Springer , ??? ( 2001 ) bchapter

    2001

  60. [68]

    , Hoek , W

    bbook Ditmarsch , H. , Hoek , W. , Kooi , B. : Dynamic Epistemic Logic . Springer , ??? ( 2007 ) bbook

    2007

  61. [69]

    , Suttner , C.B

    barticle Sutcliffe , G. , Suttner , C.B. : Evaluating General Purpose Automated Theorem Proving Systems . Artificial Intelligence 131 ( 1-2 ), 39 -- 54 ( 2001 ) 10.1016/S0004-3702(01)00113- barticle

    2001 doi

  62. [70]

    : Modern Logic

    bbook Forbes , G. : Modern Logic. A Text in Elementary Symbolic Logic . Oxford University Press , ??? ( 1994 ) bbook

    1994

  63. [71]

    : Modal Logics and Philosophy

    bbook Girle , R.A. : Modal Logics and Philosophy . Acumen Publishers , ??? ( 2000 ) bbook

    2000

  64. [72]

    : Logic for Philosophy

    bbook Sider , T. : Logic for Philosophy . Oxford University Press , ??? ( 2010 ) bbook

    2010

  65. [73]

    : What Should a Database Know? Journal of Logic Programming 14 ( 1-2 ), 127 -- 153 ( 1992 ) barticle

    barticle Reiter , R. : What Should a Database Know? Journal of Logic Programming 14 ( 1-2 ), 127 -- 153 ( 1992 ) barticle

    1992

  66. [74]

    , Herzig , A

    bchapter Cerro , L. , Herzig , A. , Longin , D. , Rifi , O. : Belief Reconstruction in Cooperative Dialogues . In: Giunchiglia , F. (ed.) Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, SYstems, and Applications . Lecture Notes in Compu...

    1998

  67. [75]

    : Towards a Computational Account of Knowledge, Action and Inference in Instructions

    barticle Stone , M. : Towards a Computational Account of Knowledge, Action and Inference in Instructions . Journal of Language and Computation 1 , 231 -- 246 ( 2000 ) barticle

    2000

  68. [76]

    , Nalon , C

    bchapter Papacchini , F. , Nalon , C. , Hustadt , U. , Dixon , C. : Efficient Local Reductions to Basic Modal Logic . In: Platzer , A. , Sutcliffe , G. (eds.) Proceedings of the 28th International Conference on Automated Deduction . Lecture Notes in Computer Science , pp. 76 -...

    2021

  69. [77]

    u ller , C. , Woltzenlogel Paleo , B. : Automating G \

    bchapter Benzm \"u ller , C. , Woltzenlogel Paleo , B. : Automating G \"o del's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers . In: Schaub , T. (ed.) Proceedings of the 21st European Conference on Artificial Intelligence , pp. 93 -- 98 ( 2014...

    2014

  70. [78]

    , Ravishankar Sarma , A.V

    barticle Mishra , M. , Ravishankar Sarma , A.V. : Tolerating Inconsistencies: A Study of Logic of Moral Conflicts . Bulletin of the Section of Logic 51 ( 2 ), 177 -- 195 ( 2022 ) barticle

    2022

  71. [79]

    , Hustadt , U

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

    2020

  72. [80]

    : The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics

    bchapter Otten , J. : The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics . In: Das , A. , Negri , S. (eds.) Proceedings of the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods . Lecture Notes in Arti...

    2021

  73. [81]

    : MleanCoP: A Connection Prover for First-Order Modal Logic

    bchapter Otten , J. : MleanCoP: A Connection Prover for First-Order Modal Logic . In: Demri , S. , Kapur , D. , Weidenbach , C. (eds.) Proceedings of the 7th International Joint Conference on Automated Reasoning . Lecture Notes in Artificial Intelligence , pp. 269 -- 276 ( 201...

    2014

  74. [82]

    , Schmidt , R

    bchapter Tishkovsky , D. , Schmidt , R. , Khodadadi , M. : The Tableau Prover Generator MetTeL2 . In: Cerro , L. , Herzig , A. , Mengin , J. (eds.) Proceedings of the 13th European Conference on Logics in Artificial Intelligence . Lecture Notes in Computer Science , pp. 492 --...

    2012

  75. [83]

    , Benzm \"u ller , C

    barticle Steen , A. , Benzm \"u ller , C. : Extensional Higher-Order Paramodulation in Leo-III . Journal of Automated Reasoning 65 ( 6 ), 775 -- 807 ( 2021 ) barticle

    2021

  76. [84]

    , Fauthoux , D

    bchapter Cerro , L. , Fauthoux , D. , Gasquet , O. , Herzig , A. , Longin , D. , Massacci , F. : LoTREC: The Generic Tableau Prover for Modal and Description Logics . In: Gore , R. , Leitsch , A. , Nipkow , T. (eds.) Proceedings of the International Joint Conference on Automat...

    2001

  77. [85]

    , Schmidt , R

    bchapter Hustadt , U. , Schmidt , R. : MSPASS: Modal Reasoning by Translation and First-Order Resolution . In: Dyckhoff , R. (ed.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods . Lecture Notes in Artificial Intell...

    2000

  78. [86]

    , Sutcliffe , G

    bchapter Steen , A. , Sutcliffe , G. , Scholl , T. , Benzm \"u ller , C. : Solving Modal Logic Problems by Translation to Higher-order Logic . In: Herzig , A. , Luo , J. , Pardo , P. (eds.) Proceedings of the 5th International Conference on Logic and Argumentation . Lecture No...

    2023

  79. [87]

    , Voronkov , A

    bchapter Horrocks , I. , Voronkov , A. : Reasoning Support for Expressive Ontology Languages Using a Theorem Prover . In: Dix , J. , Hegner , S.J. (eds.) Proceedings of the 4th International Symposium on Foundations of Information and Knowledge Systems . Lecture Notes in Compu...

    2006

  80. [88]

    , Hustadt , U

    barticle Schmidt , R. , Hustadt , U. : The Axiomatic Translation Principle for Modal Logic . ACM Transactions on Compututational Logic 8 ( 4 ), 19 ( 2007 ) barticle

    2007

  81. [89]

    , Sutcliffe , G

    bchapter Schneidner , M. , Sutcliffe , G. : Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving . In: Bj rner , N. , Sofronie-Stokkermans , V. (eds.) Proceedings of the 23rd International Conference on Automated Deduction . Lecture Notes i...

    2011

  82. [90]

    , Alassaf , R

    bchapter Eisenhofer , C. , Alassaf , R. , Rawson , M. , Kovács , L. : Non-Classical Logics in Satisfiability Modulo Theories . In: Ramanayake , D. , Urban , J. (eds.) Proceedings of the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Met...

    2023

  83. [91]

    , Paulson , L

    barticle Benzm \"u ller , C. , Paulson , L. : Quantified Multimodal Logics in Simple Type Theory . Logica Universalis 7 ( 1 ), 7 -- 20 ( 2013 ) barticle

    2013

  84. [92]

    , Raths , T

    bchapter Benzm \"u ller , C. , Raths , T. : HOL Based First-order Modal Logic Provers . In: McMillan , K. , Middeldorp , A. , Voronkov , A. (eds.) Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning . Lecture Notes ...

    2013

  85. [93]

    : Dynamic Epistemic Logic I: Modeling Knowledge and Belief

    barticle Pacuit , E. : Dynamic Epistemic Logic I: Modeling Knowledge and Belief . Philosophy Compass 8 ( 9 ), 798 -- 814 ( 2013 ) barticle

    2013

  86. [94]

    , Jones , A

    botherref Carmo , J. , Jones , A. : Completeness and Decidability Results for a Logic of Contrary-to-duty Conditionals . Journal of Logic and Computation 23(3) (2013) botherref

    2013

  87. [95]

    : Deontic Logic

    bchapter qvist , L. : Deontic Logic . In: Gabbay , D. , Guenthner , F. (eds.) Handbook of Philosophical Logic vol. 8 , pp. 147 -- 264 . Springer , ??? ( 2002 ) bchapter

    2002

  88. [96]

    , Sutcliffe , G

    bchapter Steen , A. , Sutcliffe , G. , Fontaine , P. , McKeown , J. : Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic . In: Piskac , R. , Voronkov , A. (eds.) Proceedings of 24th International Conference on Logic for Prog...

    2023

  89. [97]

    , Steen , A

    botherref Sutcliffe , G. , Steen , A. , Fontaine , P. : The New TPTP Format for Interpretations . arXiv:2406.06108 (2024) botherref

    2024 arXiv

  90. [98]

    , Vaught , R

    barticle Tarski , A. , Vaught , R. : Arithmetical Extensions of Relational Systems . Compositio Mathematica 13 , 81 -- 102 ( 1956 ) barticle

    1956

  91. [99]

    : Logic for Computer Science - Foundations of Automatic Theorem Proving

    bbook Gallier , J. : Logic for Computer Science - Foundations of Automatic Theorem Proving . Dover Publications , ??? ( 2015 ) bbook

    2015

  92. [100]

    : SystemOnTPTP

    bchapter Sutcliffe , G. : SystemOnTPTP . In: McAllester , D. (ed.) Proceedings of the 17th International Conference on Automated Deduction . Lecture Notes in Artificial Intelligence , pp. 406 -- 410 . Springer , ??? ( 2000 ) bchapter

    2000

  93. [101]

    : TPTP, TSTP, CASC, etc

    bchapter Sutcliffe , G. : TPTP, TSTP, CASC, etc. In: Diekert , V. , Volkov , M. , Voronkov , A. (eds.) Proceedings of the 2nd International Symposium on Computer Science in Russia . Lecture Notes in Computer Science , pp. 6 -- 22 . Springer , ??? ( 2007 ) bchapter

    2007

  94. [102]

    : tptp-utils v1.1

    botherref Steen , A. : tptp-utils v1.1 . Zenodo (2021). 10.5281/zenodo.587756 botherref

    2021 doi

  95. [103]

    : Scala TPTP Parser v1.5

    botherref Steen , A. : Scala TPTP Parser v1.5 . Zenodo (2021). 10.5281/zenodo.557887 botherref

    2021 doi

  96. [104]

    : Semantic Derivation Verification: Techniques and Implementation

    barticle Sutcliffe , G. : Semantic Derivation Verification: Techniques and Implementation . International Journal on Artificial Intelligence Tools 15 ( 6 ), 1053 -- 1070 ( 2006 ) 10.1142/S021821300600311 barticle

    2006 doi

  97. [105]

    , Blanqui , F

    bchapter Sutcliffe , G. , Blanqui , F. , Burel , G. : Proof Verification with GDV and LambdaPi - It's a Matter of Trust . In: Biskri , I. , Talbert , D. (eds.) Proceedings of the 38th International FLAIRS Conference ( 2025 ). 10.32473/flairs.38.1.13864 bchapter

    2025 doi

  98. [106]

    , Puzis , Y

    bchapter Trac , S. , Puzis , Y. , Sutcliffe , G. : An Interactive Derivation Viewer . In: Autexier , S. , Benzm \"u ller , C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers . Electronic Notes in Theoretical Computer Science , vol. 174 , pp. 109 -...

    2007

  99. [107]

    , Sutcliffe , G

    bchapter McKeown , J. , Sutcliffe , G. : An Interactive Interpretation Viewer for Typed First-order Logic . In: Ae Chun , A. , Franklin , M. (eds.) Proceedings of the 36th International FLAIRS Conference ( 2023 ). 10.32473/flairs.36.13307 bchapter

    2023 doi

  100. [108]

    write newline

    " write newline "" before.all 'output.state := FUNCTION string.to.integer 't := t text.length 'k := #1 'char.num := t char.num #1 substring 's := s is.num s "." = or char.num k = not and char.num #1 + 'char.num := while char.num #1 - 'char.num := t #1 char.num substring FUNCTI...

Pith tools

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