{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:46:31Z","timestamp":1753886791985},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287169"},{"type":"electronic","value":"9783642287176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28717-6_32","type":"book-chapter","created":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T15:13:04Z","timestamp":1331046784000},"page":"406-419","source":"Crossref","is-referenced-by-count":29,"title":["The TPTP Typed First-Order Form with Arithmetic"],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[]},{"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Baumgartner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"32_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.: MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. Journal of Automated Reasoning\u00a044(3), 175\u2013205 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"issue":"3\/4","key":"32_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational Theorem Proving for Hierachic First-Order Theories. Applicable Algebra in Engineering, Communication and Computing\u00a05(3\/4), 193\u2013212 (1994)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"32_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010)"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"32_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: ME(LIA) - Model Evolution with Linear Integer Arithmetic Constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 258\u2013273. Springer, Heidelberg (2008)"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Pelzer, B., Tinelli, C.: Model Evolution with Equality - Revised and Implemented. Journal of Symbolic Computation (2011) (page to appear)","DOI":"10.1016\/j.jsc.2011.12.031"},{"key":"32_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C.E. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C.E., Rabe, F., Sutcliffe, G.: THF0 \u2013 The Core of the TPTP Language for Higher-Order Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 491\u2013506. Springer, Heidelberg (2008)"},{"issue":"2","key":"32_CR9","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/128861.128862","volume":"14","author":"R. Boute","year":"1992","unstructured":"Boute, R.: The Euclidean Definition of the Functions div and mod. ACM Transactions on Programming Languages and Systems\u00a014(2), 127\u2013144 (1992)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"32_CR10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.E. Brown","year":"2003","unstructured":"Brown, C.E.: QEPCAD B - A Program for Computing with Semi-algebraic sets using CADs. ACM SIGSAM Bulletin\u00a037(4), 97\u2013108 (2003)","journal-title":"ACM SIGSAM Bulletin"},{"key":"32_CR11","unstructured":"Claessen, K., S\u00f6rensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)"},{"key":"32_CR12","unstructured":"Cohn, A.G.: Many Sorted Logic = Unsorted Logic + Control? In: Bramer, M. (ed.) Proceedings of Expert Systems 1986, The 6th Annual Technical Conference on Research and Development in Expert Systems, pp. 184\u2013194. Cambridge University Press (1986)"},{"issue":"2","key":"32_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/BF00243207","volume":"3","author":"A.G. Cohn","year":"1987","unstructured":"Cohn, A.G.: A More Expressive Formulation of Many Sorted Logic. Journal of Automated Reasoning\u00a03(2), 113\u2013200 (1987)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"32_CR15","unstructured":"Gallier, J.: Logic for Computer Science: Foundations of Automated Theorem Proving. Computer Science and Technology Series. Wiley (1986)"},{"issue":"2","key":"32_CR16","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"J. Halpern","year":"1991","unstructured":"Halpern, J.: Presburger Arithmetic With Unary Predicates is $\\Pi_1^1$ -Complete. Journal of Symbolic Logic\u00a056(2), 637\u2013642 (1991)","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR17","unstructured":"Harrison, J.: Email to Cesare Tinelli"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511576430"},{"key":"32_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS (LNAI), vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"32_CR20","unstructured":"McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)"},{"issue":"2","key":"32_CR21","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T. Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear Quantifier Elimination. Journal of Automated Reasoning\u00a045(2), 189\u2013212 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR22","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a0192, pp. 19\u201333 (2006)"},{"issue":"8","key":"32_CR23","first-page":"4","volume":"31","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. Communications of the ACM\u00a031(8), 4\u201313 (1992)","journal-title":"Communications of the ACM"},{"key":"32_CR24","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Format: An Initial Proposal. In: Nebel, B., Swartout, W. (eds.) Proceedings of the Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2003)"},{"key":"32_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"32_CR26","unstructured":"Schmidt-Schauss, M.: A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 1162\u20131168 (1985)"},{"issue":"2-3","key":"32_CR27","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E: A Brainiac Theorem Prover. AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"32_CR28","unstructured":"Stickel, M.E.: SNARK - SRI\u2019s New Automated Reasoning Kit, http:\/\/www.ai.sri.com\/\u00a0stickel\/snark.html"},{"key":"32_CR29","unstructured":"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, vol.\u00a0418, pp. 38\u201349 (2008)"},{"issue":"4","key":"32_CR30","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR31","unstructured":"Sutcliffe, G.: Proceedings of the 5th IJCAR ATP System Competition. Edinburgh, United Kingdom (2010)"},{"key":"32_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP World \u2013 Infrastructure for Automated Reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 1\u201312. Springer, Heidelberg (2010)"},{"key":"32_CR33","unstructured":"Sutcliffe, G.: Proceedings of the CADE-23 ATP System Competition. Wroclaw, Poland (2011)"},{"key":"32_CR34","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The CADE-23 Automated Theorem Proving System Competition - CASC-23. AI Communications (page to appear, 2012)","DOI":"10.3233\/AIC-2012-0512"},{"key":"32_CR35","unstructured":"Sutcliffe, G., Suda, M., Teyssandier, A., Dellis, N., de Melo, G.: Progress Towards Effective Automated Reasoning with World Knowledge. In: Murray, C., Guesgen, H. (eds.) Proceedings of the 23rd International FLAIRS Conference, pp. 110\u2013115. AAAI Press (2010)"},{"key":"32_CR36","unstructured":"Walther, C.: A Many-Sorted Calculus Based on Resolution and Paramodulation. In: Bundy, A. (ed.) Proceedings of the 8th International Joint Conference on Artificial Intelligence, pp. 882\u2013891 (1983)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28717-6_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:07:19Z","timestamp":1620126439000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28717-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287169","9783642287176"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}