{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:29:29Z","timestamp":1753885769802},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745099"},{"type":"electronic","value":"9783540745105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74510-5_4","type":"book-chapter","created":{"date-parts":[[2007,8,21]],"date-time":"2007-08-21T15:11:35Z","timestamp":1187709095000},"page":"6-22","source":"Crossref","is-referenced-by-count":13,"title":["TPTP, TSTP, CASC, etc."],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Blanchet, B.: Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM (2004)","DOI":"10.1145\/1044731.1044735"},{"issue":"1","key":"4_CR2","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the Model Evolution Calculus. International Journal on Artificial Intelligence Tools\u00a015(1), 21\u201352 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"4_CR3","unstructured":"Proceedings of the Workshop on Empirically Successful Higher-Order Logic. In: 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning, vol. 0601042 of arXiv (2005)"},{"key":"4_CR4","unstructured":"Claessen, K., Sorensson, 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":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11817963_1","volume-title":"Computer Aided Verification","author":"M. Das","year":"2006","unstructured":"Das, M.: Formal Specifications on Industrial-Strength Code - From Myth to Reality. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, p. 1. Springer, Heidelberg (2006)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"894","DOI":"10.1007\/978-3-540-45236-2_48","volume-title":"FME 2003: Formal Methods","author":"E. Denney","year":"2003","unstructured":"Denney, E., Fischer, B.: Correctness of Source-level Safety Policies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 894\u2013913. Springer, Heidelberg (2003)"},{"key":"4_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-540-25984-8_12","volume-title":"Automated Reasoning","author":"E. Denney","year":"2004","unstructured":"Denney, E., Fischer, B., Schumann, J.: Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 198\u2013212. Springer, Heidelberg (2004)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Principles and Practice of Semantic Web Reasoning","year":"2005","unstructured":"Fages, F., Soliman, S. (eds.): PPSWR 2005. LNCS, vol.\u00a03703. Springer, Heidelberg (2005)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T.: Citius altius fortius: Lessons Learned from the Theorem Prover Waldmeister. In: Dahn, I., Vigneron, L. (eds.) Proceedings of the 4th International Workshop on First-Order Theorem Proving. Electronic Notes in Theoretical Computer Science, vol.\u00a086.1 (2003)","DOI":"10.1016\/S1571-0661(04)80649-2"},{"key":"4_CR10","volume-title":"Hardware Design Verification: Simulation and Formal Method-Based Approaches","author":"W. Lam","year":"2005","unstructured":"Lam, W.: Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall, Englewood Cliffs (2005)"},{"issue":"3","key":"4_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W.W. McCune","year":"1997","unstructured":"McCune, W.W.: Solution of the Robbins Problem. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Mace4 Reference Manual and Guide. Technical Report ANL\/MCS-TM-264, Argonne National Laboratory, Argonne, USA (2003)","DOI":"10.2172\/822574"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Mitchell, J.: Security Analysis of Network Protocols: Logical and Computational Methods. In: Barahona, P., Felty, A. (eds.) Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 151\u2013152 (2005)","DOI":"10.1145\/1069774.1069788"},{"key":"4_CR14","unstructured":"Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An Introduction to the Syntax and Content of Cyc. In: Baral, C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp. 44\u201349 (2006)"},{"key":"4_CR15","unstructured":"Meng, J., Paulson, L.: Translating Higher-Order Problems to First-Order Clauses. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, CEUR Workshop Proceedings, vol.\u00a0192, pp. 70\u201380 (2006)"},{"issue":"4","key":"4_CR16","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.websem.2004.06.002","volume":"1","author":"D. McGuinness","year":"2004","unstructured":"McGuinness, D., Pinheiro da Silva, P.: Explaining Answers from the Semantic Web: The Inference Web Approach. Journal of Web Semantics\u00a01(4), 397\u2013413 (2004)","journal-title":"Journal of Web Semantics"},{"issue":"2-3","key":"4_CR17","first-page":"77","volume":"15","author":"R. Nieuwenhuis","year":"2002","unstructured":"Nieuwenhuis, R.: The Impact of CASC in the Development of Automated Deduction Systems. AI Communications\u00a015(2-3), 77\u201378 (2002)","journal-title":"AI Communications"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Niles, I., Pease, A.: Towards A Standard Upper Ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems, pp. 2\u20139 (2001)","DOI":"10.1145\/505168.505170"},{"key":"4_CR19","unstructured":"Pease, A.: The Sigma Ontology Development Environment. In: Giunchiglia, F., Gomez-Perez, A., Pease, A., Stuckenschmidt, H., Sure, Y., Willmott, S. (eds.) Proceedings of the IJCAI-03 Workshop on Ontologies and Distributed Systems, CEUR Workshop Proceedings, vol.\u00a071 (2003)"},{"key":"4_CR20","first-page":"49","volume-title":"Proceedings of the 19th International FLAIRS Conference","author":"Y. Puzis","year":"2006","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated Generation of Interesting Theorems. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 49\u201354. AAAI Press, Stanford, California, USA (2006)"},{"key":"4_CR21","unstructured":"Pease, A., Sutcliffe, G.: First Order Reasoning on a Large Ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (2007)"},{"key":"4_CR22","volume-title":"Automated Development of Fundamental Mathematical Theories","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, Dordrecht (1992)"},{"key":"4_CR23","unstructured":"Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base. In: Shvaiko, P. (ed.) Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (2005)"},{"key":"4_CR24","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical Report Technical Report, Department of Computer Science, The University of Iowa, Iowa City, USA (2006)"},{"key":"4_CR25","unstructured":"Rudnicki, P.: An Overview of the Mizar Project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311\u2013332 (1992)"},{"issue":"2-3","key":"4_CR26","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"4_CR27","first-page":"14","volume-title":"Proceedings of the 19th International FLAIRS Conference","author":"M. Sahami","year":"2006","unstructured":"Sahami, M.: Mining the Web to Determine Similarity Between Words, Objects, and Communities. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 14\u201319. AAAI Press, Stanford, California, USA (2006)"},{"issue":"2-3","key":"4_CR28","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"},{"issue":"2","key":"4_CR29","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0898-1221(94)00219-B","volume":"29","author":"J.K. Slaney","year":"1995","unstructured":"Slaney, J.K., Fujita, M., Stickel, M.E.: Automated Reasoning and Exhaustive Search: Quasigroup Existence Problems. Computers and Mathematics with Applications\u00a029(2), 115\u2013132 (1995)","journal-title":"Computers and Mathematics with Applications"},{"key":"4_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Proceedings of the 21st International Conference on Automated Deduction","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS - a Semantic Relevance Axiom Selection System. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction. LNCS (LNAI), vol.\u00a04603, pp. 295\u2013310. Springer, Heidelberg (2007)"},{"issue":"2","key":"4_CR31","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR32","first-page":"341","volume-title":"Proceedings of the 12th International FLAIRS Conference","author":"G. Sutcliffe","year":"1999","unstructured":"Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th International FLAIRS Conference, pp. 341\u2013345. AAAI Press, Stanford, California, USA (1999)"},{"issue":"1-2","key":"4_CR33","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G. Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.B.: Evaluating General Purpose Automated Theorem Proving Systems. Artificial Intelligence\u00a0131(1-2), 39\u201354 (2001)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"4_CR34","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"key":"4_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G. Sutcliffe","year":"2006","unstructured":"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.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 67\u201381. Springer, Heidelberg (2006)"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/10721959_31","volume-title":"Automated Deduction - CADE-17","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 406\u2013410. Springer, Heidelberg (2000)"},{"issue":"6","key":"4_CR37","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools\u00a015(6), 1053\u20131070 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"4_CR38","unstructured":"Sutcliffe, G.: The TSTP Solution Library. http:\/\/www.TPTP.org\/TSTP"},{"key":"4_CR39","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"201","volume-title":"Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems","author":"G. Sutcliffe","year":"2004","unstructured":"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 Applications, vol.\u00a0112, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An Interactive Derivation Viewer. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proceedings of the 7th Workshop on Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning. Electronic Notes in Theoretical Computer Science, vol.\u00a0174, pp. 109\u2013123 (2006)","DOI":"10.1016\/j.entcs.2006.09.025"},{"issue":"1-2","key":"4_CR41","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2007","unstructured":"Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning\u00a037(1-2), 21\u201343 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR42","unstructured":"Urban, J., Sutcliffe, G.: The MPTP $100 Challenges (2006), http:\/\/www.tptp.org\/MPTPChallenge\/"},{"key":"4_CR43","unstructured":"Urban, J., Trac, S., Sutcliffe, G., Puzis, Y.: Combining Mizar and TPTP Semantic Presentation Tools. In: Proceedings of the Mathematical User-Interfaces Workshop 2007 (2007)"},{"key":"4_CR44","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814771_15","volume-title":"Automated Reasoning","author":"A. Gelder Van","year":"2006","unstructured":"Van Gelder, A., Sutcliffe, G.: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 156\u2013161. Springer, Heidelberg (2006)"},{"key":"4_CR45","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D., SPASS,: SPASS Version 2.0. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Science \u2013 Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74510-5_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:21:58Z","timestamp":1619518918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74510-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745099","9783540745105"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74510-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}