{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:58Z","timestamp":1776333418893,"version":"3.51.2"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,9,15]],"date-time":"2007-09-15T00:00:00Z","timestamp":1189814400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2008,1]]},"DOI":"10.1007\/s10817-007-9085-y","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T12:19:44Z","timestamp":1189772384000},"page":"35-60","source":"Crossref","is-referenced-by-count":72,"title":["Translating Higher-Order Clauses to First-Order Clauses"],"prefix":"10.1007","volume":"40","author":[{"given":"Jia","family":"Meng","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,9,15]]},"reference":[{"issue":"4","key":"9085_CR1","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/s10817-006-9036-z","volume":"36","author":"M. Beeson","year":"2006","unstructured":"Beeson, M.: Mathematical induction in Otter-lambda. J. Autom. Reason. 36(4), 311\u2013344 (2006)","journal-title":"J. Autom. Reason."},{"key":"9085_CR2","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Can a higher-order and a first-order theorem prover cooperate? In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning \u2013 11th International Workshop, LPAR 2004, LNAI, vol. 3452, pp. 415\u2013431. Springer (2005)","DOI":"10.1007\/978-3-540-32275-7_27"},{"key":"9085_CR3","doi-asserted-by":"crossref","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 4349, pp. 74\u201388. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_5"},{"key":"9085_CR4","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge Univ. Press (1993)"},{"key":"9085_CR5","doi-asserted-by":"crossref","unstructured":"Hughes, R.J.M.: Supercombinators: a new implementation method for applicative languages. In: LISP and Func. Prog. ACM Press (1982)","DOI":"10.1145\/800068.802129"},{"key":"9085_CR6","doi-asserted-by":"crossref","unstructured":"Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) Automated Deduction \u2013 CADE-18 International Conference, LNAI, vol. 2392, pp. 134\u2013138. Springer (2002)","DOI":"10.1007\/3-540-45620-1_10"},{"key":"9085_CR7","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, Number NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368, September (2003)"},{"issue":"4","key":"9085_CR8","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1145\/48022.48026","volume":"10","author":"R. Kennaway","year":"1988","unstructured":"Kennaway, R., Sleep, R.: Director strings as combinators. ACM Trans. Program. Lang. Syst. 10(4), 602\u2013626 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9085_CR9","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order problems to first-order clauses. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings, vol. 192, pp. 70\u201380 (2006)"},{"key":"9085_CR10","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic (2007) (in press)"},{"issue":"10","key":"9085_CR11","doi-asserted-by":"crossref","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: first prototype. Inf. Comput. 204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"issue":"4","key":"9085_CR12","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321\u2013358 (1992)","journal-title":"J. Symb. Comput."},{"key":"9085_CR13","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a Proof Assistant for Higher-Order Logic. LNCS Tutorial, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9085_CR14","doi-asserted-by":"crossref","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification: 8th International Conference, CAV \u201996, LNCS, vol. 1102, pp. 411\u2013414. Springer (1996)","DOI":"10.1007\/3-540-61474-5_91"},{"key":"9085_CR15","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Klaus, S., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, LNCS, vol. 4732, pp. 232\u2013245. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"9085_CR16","unstructured":"Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice Hall (1987)"},{"key":"9085_CR17","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press (2002)"},{"key":"9085_CR18","doi-asserted-by":"crossref","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) Automated Reasoning \u2013 First International Joint Conference, IJCAR 2001, LNAI, vol. 2083, pp. 376\u2013380. Springer (2001)","DOI":"10.1007\/3-540-45744-5_29"},{"key":"9085_CR19","doi-asserted-by":"crossref","unstructured":"Schulz, S.: System description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) Automated Reasoning \u2013 Second International Joint Conference, IJCAR 2004, LNAI, vol. 3097, pp. 223\u2013228. Springer (2004)","DOI":"10.1007\/978-3-540-25984-8_15"},{"key":"9085_CR20","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library for automated theorem proving. On the internet at http:\/\/www.cs.miami.edu\/~tptp\/ (2004)"},{"key":"9085_CR21","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, Number 112 in Frontiers in Artificial Intelligence and Applications, pp. 201\u2013215. IOS Press (2004)"},{"issue":"2","key":"9085_CR22","doi-asserted-by":"crossref","first-page":"267","DOI":"10.2307\/2273733","volume":"44","author":"D.A. Turner","year":"1979","unstructured":"Turner, D.A.: Another algorithm for bracket abstraction. J. Symb. Log. 44(2), 267\u2013270, June 1979","journal-title":"J. Symb. Log."},{"key":"9085_CR23","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1002\/spe.4380090105","volume":"9","author":"D.A. Turner","year":"1979","unstructured":"Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Exp. 9, 31\u201349 (1979)","journal-title":"Softw. Pract. Exp."},{"key":"9085_CR24","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, chapter\u00a027, pp. 1965\u20132013. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"9085_CR25","unstructured":"Zimmer, J., Meier, A., Sutcliffe, G., Zhang, Y.: Integrated proof transformation services. In: Benzm\u00fcller, C., Windsteiger, W. (eds.) Workshop on Computer-Supported Mathematical Theory Development, 2nd International Joint Conference on Automated Reasoning, Electronic Notes in Theoretical Computer Science (2004)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9085-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9085-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9085-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:48Z","timestamp":1559265708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9085-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9,15]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["9085"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9085-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9,15]]}}}