{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:52Z","timestamp":1747592452107},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_7","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"67-81","source":"Crossref","is-referenced-by-count":27,"title":["Using the TPTP Language for Writing Derivations and Finite Interpretations"],"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":"Allen","family":"Van Gelder","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11541868_5","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Benzm\u00fcller","year":"2005","unstructured":"Benzm\u00fcller, C., Brown, C.: A Structured Set of Higher-Order Problems. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 66\u201381. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Caprotti, O., Carlisle, D.: OpenMath and MathML: Semantic Mark Up for Mathematics. ACM Crossroads\u00a06(2) (1999)","key":"7_CR2","DOI":"10.1145\/333104.333110"},{"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":"7_CR3"},{"key":"7_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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":"7_CR5","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1006\/jsco.1996.0029","volume":"21","author":"J. Denzinger","year":"1996","unstructured":"Denzinger, J., Schulz, S.: Recording and Analysing Knowledge-Based Distributed Deduction Processes. Journal of Symbolic Computation\u00a021, 523\u2013541 (1996)","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR6","volume-title":"Introduction to HOL, a Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"unstructured":"H\u00e4hnle, R., Kerber, M., Weidenbach, C.: Common Syntax of the DFG-Schwerpunktprogramm Deduction. Technical Report TR 10\/96, Fakult\u00e4t f\u00fcr Informatik, Univers\u00e4t Karlsruhe, Karlsruhe, Germany (1996)","key":"7_CR7"},{"unstructured":"Hurd, J., Arthan, R.: OpenTheory, http:\/\/www.cl.cam.ac.uk\/jeh1004\/research\/opentheory","key":"7_CR8"},{"key":"7_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-44990-6_3","volume-title":"Artificial Intelligence and Symbolic Computation","author":"M. Kohlhase","year":"2001","unstructured":"Kohlhase, M.: OMDOC: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge. In: Campbell, J.A., Roanes-Lozano, E. (eds.) AISC 2000. LNCS (LNAI), vol.\u00a01930, pp. 32\u201352. Springer, Heidelberg (2001)"},{"key":"7_CR10","series-title":"Advances in Formal Methods","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-1-4757-3188-0_16","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"W. McCune","year":"2000","unstructured":"McCune, W., Shumsky-Matlin, O.: Ivy: A Preprocessor and Proof Checker for First-Order Logic. In: Kaufmann, M., Manolios, P., Strother Moore, J. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. Advances in Formal Methods, vol.\u00a04, pp. 265\u2013282. Kluwer Academic Publishers, Dordrecht (2000)"},{"unstructured":"McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)","key":"7_CR11"},{"issue":"2-3","key":"7_CR12","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"},{"unstructured":"Schulz, S.: LOP-Syntax for Theorem Proving Applications, http:\/\/www4.informatik.tu-muenchen.de\/~schulz\/WORK\/lop.syntax","key":"7_CR13"},{"unstructured":"Schulz, S., Bonacina, M.P.: On Handling Distinct Objects in the Superposition Calculus. In: Konev, B., Schulz, S. (eds.) Proceedings of the 5th International Workshop on the Implementation of Logics, pp. 66\u201377 (2005)","key":"7_CR14"},{"unstructured":"Steel, G.: Visualising First-Order Proof Search. In: Aspinall, C., L\u00fcth, D. (eds.) Proceedings of User Interfaces for Theorem Provers 2005, pp. 179\u2013189 (2005)","key":"7_CR15"},{"key":"7_CR16","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.) CADE 2000. LNCS, vol.\u00a01831, pp. 406\u2013410. Springer, Heidelberg (2000)"},{"unstructured":"Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools ( page to appear, 2006)","key":"7_CR17"},{"unstructured":"Sutcliffe, G.: The TSTP Solution Library, http:\/\/www.TPTP.org\/TSTP","key":"7_CR18"},{"issue":"2","key":"7_CR19","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":"7_CR20","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)"},{"issue":"3-4","key":"7_CR21","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J. Urban","year":"2004","unstructured":"Urban, J.: MPTP - Motivation, Implementation, First Experiments. Journal of Automated Reasoning\u00a033(3-4), 319\u2013339 (2004)","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Van Gelder, A., Sutcliffe, G.: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. In: Furbach, U., Shankar, N. (eds.) IWSM 2000 (2006)","key":"7_CR22","DOI":"10.1007\/11814771_15"},{"unstructured":"Zimmer, J.: A New Framework for Reasoning Agents. In: Sorge, V., Colton, S., Fisher, M., Gow, J. (eds.) Proceedings of the Workshop on Agents and Automated Reasoning, 18th International Joint Conference on Artificial Intelligence, pp. 58\u201364 (2003)","key":"7_CR23"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T09:52:49Z","timestamp":1555840369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11814771_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}