{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:50Z","timestamp":1761611150032},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf01063152","type":"journal-article","created":{"date-parts":[[2005,1,29]],"date-time":"2005-01-29T15:00:01Z","timestamp":1107010801000},"page":"199-230","source":"Crossref","is-referenced-by-count":6,"title":["A note on the proof theory the ?II-calculus"],"prefix":"10.1007","volume":"54","author":[{"given":"David J.","family":"Pym","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1305\/ndjfl\/1093635337","volume":"31","author":"A. Avron","year":"1990","unstructured":"Avron, A., 1990, ?Gentzenizing Schroeder-Heister's Natural Extension of Natural Deduction?,Notre Dame J. of Formal Logic 31, 127?135.","journal-title":"Notre Dame J. of Formal Logic"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"Avron, A., F. Honsell, I.A. Mason and R. Pollack, 1992, ?Using Typed Lambda Calculus to Implement Formal Systems on a Machine?,J. Automated Reasoning 9, 309?354.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"CR3","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"Barendregt, H., 1991, ?Introduction to generalized type systems?,J. Func. Prog. 1(2), 125?154.","journal-title":"J. Func. Prog."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"Cartmell, J., 1986, ?Generalized Algebraic Theories and Contextual Categories?,Annals of Pure and Applied Logic 32, 209?243.","journal-title":"Annals of Pure and Applied Logic"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Clocksin, W. F., C.S. Mellish, 1984,Programming in Prolog, Springer-Verlag.","DOI":"10.1007\/978-3-642-96661-3"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Coquand, Th., 1991, ?An Algorithm for testing conversion in type theory?, in: G. Huet and G. Plotkin (editors),Logical Frameworks. Cambridge University Press, 255?279.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"CR7","unstructured":"Daalen, D. T. van, 1980,The Language Theory of AUTOMATH. Ph.D. thesis, Technical University of Eindhoven."},{"key":"CR8","unstructured":"Dowek, G., 1991,D\ufffdmonstration Automatique dans le Calcul des Constructions. Th\ufffdse de Doctorat, Universit\ufffd de Paris 7."},{"key":"CR9","unstructured":"Elliott, C. M., 1990,Extensions and Applications of Higher-order Unification. Ph.D. thesis, School of Computer Science, Carnegie Mellon University. Available as Technical Report CMU-CS-90-134."},{"key":"CR10","unstructured":"Felty, A., 1987, ?Implementing Theorem Provers in Logic Programming?, University of Pennsylvania report MS-CIS-87-109."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G., 1934, ?Untersuchungen \ufffdber das logische Schliessen?,Mathematische Zeitschrift 39, 176?210, 405?431.","journal-title":"Mathematische Zeitschrift"},{"key":"CR12","unstructured":"Harper, R. 1988, ?An Equational Formulation oflf?, LFCS, report ECS-LFCS-88-67, University of Edinburgh."},{"key":"CR13","unstructured":"Harper, R., F. Honsell, G. Plotkin 1987, ?A Framework for Defining Logics?,Proc. Second Annual Symposium on Logic in Computer Science, 194?204. IEEE."},{"issue":"1","key":"CR14","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., F. Honsell, G. Plotkin, 1993, ?A Framework for Defining Logics?,J. ACM Vol. 40, No. 1, January, 143?184.","journal-title":"J. ACM"},{"key":"CR15","unstructured":"Hindley, J. R. and J. P. Seldin, 1986,Introduction to Combinators and ?-Calculus. Cambridge University Press."},{"key":"CR16","unstructured":"Howard, W. A., 1980, ?The formulae-as-types notion of construction?, in:To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (editors J.P. Seldin & J.R. Hindley), Academic Press."},{"key":"CR17","unstructured":"Kleene, S. C., 1968,Mathematical Logic. Wiley and Sons."},{"key":"CR18","unstructured":"Martin-L\ufffdf, P., 1985, ?On the meanings of the logical constants and the justifications of the logical laws?, Technical Report 2, Scuola di Specializziazione in Logica Matematica, Dipartimento di Matematica, Universit\ufffd di Siena."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. Meyer","year":"1982","unstructured":"Meyer, A., 1982, ?What is a Model of the Lambda Calculus?Information and Control 52, 87?122.","journal-title":"Information and Control"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., G. Nadathur, A. ??edrov and F. Pfenning, 1991, ?Uniform Proofs as a Foundation for Logic Programming?,Ann. Pure and Appl. Logic 51, 125?157.","journal-title":"Ann. Pure and Appl. Logic"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"Pfenning, F., 1991, ?Logic programming in the LF logical framework?, in: G. Huet and G. Plotkin (editors),Logical Frameworks, Cambridge University Press, 149?181.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"CR22","unstructured":"Prawitz, D. 1965,Natural deduction: a proof-theoretical study. Almqvist & Wiksell."},{"key":"CR23","unstructured":"Pym, D. J., 1990,Proofs, Search and Computation in General Logic. Ph.D. thesis, University of Edinburgh, 1990. Available as report CST-69-90, Department of Computer Science, University of Edinburgh. (Also published as LFCS report ECS-LFCS-90-125.)"},{"issue":"3","key":"CR24","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1142\/S012905419200019X","volume":"3","author":"D. J. Pym","year":"1992","unstructured":"Pym, D. J., 1992, ?A Unification Algorithm for the ?II-calculus?,Int. J. of Foundations of Computer Science, Vol. 3, No. 3, 333?378.","journal-title":"Int. J. of Foundations of Computer Science"},{"key":"CR25","first-page":"236","volume":"449","author":"D. J. Pym","year":"1990","unstructured":"Pym, D. J. and L. A. Wallen, 1990, ?Investigations into Proof-search in a system of first-order dependent function types?,Proc. 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 1990, M. Stickel (editor), Lecture Notes in Artificial Intelligence449, 236?250, Springer-Verlag.","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Pym, D. J. and L. A. Wallen, 1991, ?Proof-search in the ?II-calculus?, in: G. Huet and G. Plotkin (editors),Logical Frameworks, Cambridge University Press, 309?340.","DOI":"10.1017\/CBO9780511569807.013"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"Pym, D. J. and L. A. Wallen, 1992, ?Logic Programming via Proof-valued Computations?, in:ALPUK92, Proc. of the 4th U.K. Conference on Logic Programming, K. Broda (editor), 253?262. Springer-Verlag.","DOI":"10.1007\/978-1-4471-3421-3_14"},{"key":"CR28","unstructured":"Pym, D. J., 1993, ?Errata and Remarks?, LFCS Report ECS-LFCS-93-265. University of Edinburgh."},{"key":"CR29","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"Robinson, J., 1965, ?A machine-oriented logic based on the resolution principle?,J. Assoc. Comp. Mach. 12, 23?41.","journal-title":"J. Assoc. Comp. Mach."},{"key":"CR30","unstructured":"Salvesen, A., 1989, Manuscript, University of Edinburgh."},{"key":"CR31","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P. Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P., 1984, ?A Natural Extension of Natural Deduction?,J. Symb. Log. 49, 1284?1299.","journal-title":"J. Symb. Log."},{"key":"CR32","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF01621477","volume":"30","author":"W. Sieg","year":"1991","unstructured":"Sieg, W., 1991, ?Herbrand analyses?,Arch. Math. Logic 30, 409?441.","journal-title":"Arch. Math. Logic"},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"Smullyan, R. M., 1968, ?First-order logic?,Ergebnisse der Mathematik 43, Springer-Verlag.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. Zucker","year":"1974","unstructured":"Zucker, J., 1974, ?The correspondence between cut-elimination and normalisation?,Ann. Math. Logic 7 1?112.","journal-title":"Ann. Math. Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01063152.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01063152\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01063152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T13:42:07Z","timestamp":1586094127000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01063152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF01063152"],"URL":"https:\/\/doi.org\/10.1007\/bf01063152","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}