{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T04:40:13Z","timestamp":1768452013433,"version":"3.49.0"},"reference-count":42,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T00:00:00Z","timestamp":1662940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,11,27]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The Thousands of Problems for Theorem Provers (TPTP) World is a well-established infrastructure that supports research, development and deployment of automated theorem proving systems. This paper provides an overview of the logic languages of the TPTP World, from classical first-order form (FOF), through typed FOF, up to typed higher-order form, and beyond to non-classical forms. The logic languages are described in a non-technical way and are illustrated with examples using the TPTP language.<\/jats:p>","DOI":"10.1093\/jigpal\/jzac068","type":"journal-article","created":{"date-parts":[[2022,9,13]],"date-time":"2022-09-13T16:31:20Z","timestamp":1663086680000},"page":"1153-1169","source":"Crossref","is-referenced-by-count":17,"title":["The logic languages of the TPTP world"],"prefix":"10.1093","volume":"31","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[{"name":"Department of Computer Science , University of Miami, Coral Gables, Florida, 33146, USA"}]}],"member":"286","published-online":{"date-parts":[[2022,9,12]]},"reference":[{"key":"2023112820225600100_ref1","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth through Proof","author":"Andrews","year":"1986"},{"key":"2023112820225600100_ref2","first-page":"462","article-title":"Basic paramodulation and superposition","volume-title":"Proceedings of the 11th International Conference on Automated Deduction","author":"Bachmair","year":"1992"},{"key":"2023112820225600100_ref3","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","article-title":"Resolution theorem proving","volume-title":"Handbook of Automated Reasoning","author":"Bachmair","year":"2001"},{"key":"2023112820225600100_ref4","volume-title":"Normal Multimodal Logics: Automatic Deduction and Logic Programming Extensions","author":"Baldoni","year":"1998"},{"key":"2023112820225600100_ref5","first-page":"396","article-title":"Superposition for full higher-order logic","author":"Bentkamp","year":"2021","journal-title":"Proceedings of the 28th International Conference on Automated Deduction"},{"key":"2023112820225600100_ref6","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","article-title":"Higher-order semantics and extensionality","volume":"69","author":"Benzm\u00fcller","year":"2004","journal-title":"Journal of Symbolic Logic"},{"key":"2023112820225600100_ref7","first-page":"984","volume-title":"Handbook of Modal Logic","author":"Blackburn","year":"2006"},{"key":"2023112820225600100_ref8","first-page":"414","article-title":"TFF1: The TPTP typed first-order form with rank-1 polymorphism","volume-title":"Proceedings of the 24th International Conference on Automated Deduction","author":"Blanchette","year":"2013"},{"key":"2023112820225600100_ref9","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF00243207","article-title":"A more expressive formulation of many sorted logic","volume":"3","author":"Cohn","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"2023112820225600100_ref10","volume-title":"A Mathematical Introduction to Logic","author":"Enderton","year":"1972"},{"key":"2023112820225600100_ref11","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-Order Modal Logic","author":"Fitting","year":"1998"},{"key":"2023112820225600100_ref12","article-title":"Temporal logic","volume-title":"Stanford Encyclopedia of Philosophy","author":"Goranko","year":"2022"},{"key":"2023112820225600100_ref13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"Harel","year":"2000"},{"key":"2023112820225600100_ref14","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"Journal of the ACM"},{"key":"2023112820225600100_ref15","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"Journal of Symbolic Logic"},{"key":"2023112820225600100_ref16","first-page":"41","article-title":"TH1: The TPTP typed higher-order form with rank-1 polymorphism","volume-title":"Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning","author":"Kaliszyk","year":"2016"},{"key":"2023112820225600100_ref17","first-page":"71","article-title":"A first class boolean Sort in first-order theorem proving and TPTP","volume-title":"Proceedings of the International Conference on Intelligent Computer Mathematics","author":"Kotelnikov","year":"2015"},{"key":"2023112820225600100_ref18","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-3-319-94205-6_27","article-title":"A FOOLish encoding of the next state relations of imperative programs","volume-title":"Proceedings of the 9th International Joint Conference on Automated Reasoning","author":"Kotelnikov","year":"2018"},{"key":"2023112820225600100_ref19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","article-title":"First-order theorem proving and vampire","volume-title":"Proceedings of the 25th International Conference on Computer Aided Verification","author":"Kovacs","year":"2013"},{"key":"2023112820225600100_ref20","volume-title":"Naming and Necessity: Lectures Given to the Princeton University Philosophy Colloquium","author":"Kripke","year":"1980"},{"key":"2023112820225600100_ref21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-7288-6","volume-title":"Introduction to Mathematical Logic","author":"Mendelson","year":"1987"},{"key":"2023112820225600100_ref22","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","article-title":"Computing small clause normal forms","volume-title":"Handbook of Automated Reasoning","author":"Nonnengart","year":"2001"},{"key":"2023112820225600100_ref23","first-page":"147","article-title":"Strong and weak points of the Muscadet theorem prover","volume":"15","author":"Pastre","year":"2002","journal-title":"AI Communications"},{"key":"2023112820225600100_ref24","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1023\/A:1005035316026","article-title":"Automated natural deduction in THINKER","volume":"60","author":"Pelletier","year":"1998","journal-title":"Studia Logica"},{"key":"2023112820225600100_ref25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"key":"2023112820225600100_ref26","first-page":"1162","article-title":"A many-sorted calculus with polymorphic functions based on resolution and paramodulation","volume-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence","author":"Schmidt-Schauss","year":"1985"},{"key":"2023112820225600100_ref27","first-page":"495","article-title":"Stronger: E 2.3","volume-title":"Proceedings of the 27th International Conference on Automated Deduction","author":"Schulz","year":"2019"},{"key":"2023112820225600100_ref28","article-title":"Automated reasoning in non-classical logics in the TPTP world","volume-title":"Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning","author":"Steen","year":"2022"},{"key":"2023112820225600100_ref29","first-page":"38","article-title":"The SZS ontologies for automated reasoning software","volume-title":"Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics","author":"Sutcliffe","year":"2008"},{"key":"2023112820225600100_ref30","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"2023112820225600100_ref31","first-page":"1","article-title":"The TPTP world\u2014Infrastructure for automated reasoning","volume-title":"Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning","author":"Sutcliffe","year":"2010"},{"key":"2023112820225600100_ref32","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","article-title":"The CADE ATP system competition\u2014CASC","volume":"37","author":"Sutcliffe","year":"2016","journal-title":"AI Magazine"},{"key":"2023112820225600100_ref33","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","article-title":"The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0","volume":"59","author":"Sutcliffe","year":"2017","journal-title":"Journal of Automated Reasoning"},{"key":"2023112820225600100_ref34","first-page":"1","article-title":"Automated reasoning in higher-order logic using the TPTP THF infrastructure","volume":"6355","author":"Sutcliffe","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"2023112820225600100_ref35","first-page":"72","article-title":"TFX: The TPTP extended typed first-order form","volume-title":"Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning","author":"Sutcliffe","year":"2018"},{"key":"2023112820225600100_ref36","first-page":"70","article-title":"Prolog-D-Linda: An embedding of Linda in SICStus prolog","volume-title":"Proceedings of the Joint Workshop on Distributed and Parallel Implementation of Logic Programming Systems","author":"Sutcliffe","year":"1992"},{"key":"2023112820225600100_ref37","first-page":"406","article-title":"The TPTP typed first-order form with arithmetic","volume-title":"Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning","author":"Sutcliffe","year":"2012"},{"key":"2023112820225600100_ref38","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/11814771_7","article-title":"Using the TPTP language for writing derivations and finite interpretations","volume-title":"Proceedings of the 3rd International Joint Conference on Automated Reasoning","author":"Sutcliffe","year":"2006"},{"key":"2023112820225600100_ref39","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","article-title":"The TPTP problem library: CNF release v1.2.1","volume":"21","author":"Sutcliffe","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"2023112820225600100_ref40","first-page":"36","article-title":"Minimal deontic logics","volume":"8","author":"van Benthem","year":"2015","journal-title":"Bulletin of the Section of Logic"},{"key":"2023112820225600100_ref41","volume-title":"Handbook of Epistemic Logic","author":"van Ditmarsch","year":"2015"},{"key":"2023112820225600100_ref42","first-page":"882","article-title":"A many-sorted calculus based on resolution and paramodulation","volume-title":"Proceedings of the 8th International Joint Conference on Artificial Intelligence","author":"Walther","year":"1983"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/31\/6\/1153\/53896061\/jzac068.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/31\/6\/1153\/53896061\/jzac068.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,28]],"date-time":"2023-11-28T20:23:34Z","timestamp":1701203014000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/31\/6\/1153\/6695120"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,12]]},"references-count":42,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2022,9,12]]},"published-print":{"date-parts":[[2023,11,27]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzac068","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,12]]},"published":{"date-parts":[[2022,9,12]]}}}