{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:02Z","timestamp":1725663302783},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_91","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:44:38Z","timestamp":1330206278000},"page":"236-250","source":"Crossref","is-referenced-by-count":5,"title":["Investigations into proof-search in a system of first-order dependent function types"],"prefix":"10.1007","author":[{"given":"David","family":"Pym","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lincoln","family":"Wallen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B. Theorem-proving via general matings. J. Assoc. Comp. Mach. 28(2):193\u2013214, 1981.","journal-title":"J. Assoc. Comp. Mach."},{"key":"17_CR2","unstructured":"Avron, A., Honsell, F., Mason, I. Using Typed Lambda Calculus to Implement Formal Systems on a Machine. University of Edinburgh, 1987, ECS-LFCS-87-31."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Bibel, W. Computationally Improved Versions of Herbrand's Theorem. In J. Stern, editor, Proc. of the Herbrand Symposium, Logic Colloquium '81, pp. 11\u201328, North-Holland, 1982.","DOI":"10.1016\/S0049-237X(08)71874-3"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Clocksin, W.F., Mellish, C.S. Programming in Prolog, Springer-Verlag, 1984.","DOI":"10.1007\/978-3-642-96873-0"},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"245","DOI":"10.2307\/2266612","volume":"17","author":"H.B. Curry","year":"1952","unstructured":"Curry, H.B. The permutability of rules in the classical inferential calculus. J. Symbolic Logic 17, pp. 245\u2013248, 1952.","journal-title":"J. Symbolic Logic"},{"key":"17_CR6","volume-title":"The language theory of Automath","author":"D.T. Daalen van","year":"1980","unstructured":"van Daalen, D.T., The language theory of Automath. PhD thesis, Technical University of Eindhoven, The Netherlands, 1980."},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G. Untersuchungen \u00fcber das logische Schliessen, Mathematische Zeitschrift 39 (1934) 176\u2013210, 405\u2013431.","journal-title":"Mathematische Zeitschrift"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Harper, R., Honsell, F., Plotkin, G. A Framework for Defining Logics. Proc. LICS '87.","DOI":"10.1145\/138027.138060"},{"key":"17_CR9","unstructured":"Harper, R., Honsell, F., Plotkin, G. A Framework for Defining Logics. Submitted to the J. Assoc. Comp. Mach., 1989."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Huet, G. A Unification Algorithm for Typed \u03bb-calculus. Theor. Comp. Sci., 1975.","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"17_CR11","first-page":"1","volume":"10","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C. Permutability of inferences in Gentzen's calculi LK and LJ. Memoirs of the American Mathematical Society 10, pp. 1\u201326, 1952.","journal-title":"Memoirs of the American Mathematical Society"},{"key":"17_CR12","unstructured":"Kleene, S.C. Mathematical logic. Wiley and Sons, 1968."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Meyer, A. and Reinhold, M. \u2018Type\u2019 is not a type: preliminary report. in Proc. 13th ACM Symp. on the Principles of Programming Languages, 1986.","DOI":"10.1145\/512644.512671"},{"key":"17_CR14","volume-title":"Proofs in higher-order logic","author":"D. Miller","year":"1983","unstructured":"Miller, D. Proofs in higher-order logic. PhD thesis, Carnegie-Mellon University, Pittsburgh, USA, 1983."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Ohlbach, H-J. A resolution calculus for modal logics. Proc. 9th Conf. on Automated Deduction, LNCS 310, 1988.","DOI":"10.1007\/BFb0012852"},{"key":"17_CR16","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. Paulson","year":"1986","unstructured":"Paulson, L. Natural Deduction Proof as Higher-order Resolution. J. Logic Programming 3, pp. 237\u2013258, 1986.","journal-title":"J. Logic Programming"},{"key":"17_CR17","volume-title":"Natural Deduction: A Proof-theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D. Natural Deduction: A Proof-theoretical Study. Almqvist & Wiksell, Stockholm, 1965."},{"key":"17_CR18","unstructured":"Pym, D.J. Proofs, Search and Computation in General Logic. PhD thesis. University of Edinburgh, forthcoming."},{"key":"17_CR19","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"Robinson, J. A machine-oriented logic based on the resolution principle. J. Assoc. Comp. Mach. 12, pp. 23\u201341, 1965.","journal-title":"J. Assoc. Comp. Mach."},{"key":"17_CR20","unstructured":"Salvesen, A. In preparation. University of Edinburgh, 1989."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M. First-order logic, Ergebnisse der Mathematik, Volume 43, Springer Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"17_CR22","unstructured":"Wallen, L.A. Automated deduction in non-classical logics, MIT Press, 1989."}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_91.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:39Z","timestamp":1605648339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_91"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_91","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}