{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T05:18:56Z","timestamp":1780723136642,"version":"3.54.1"},"publisher-location":"London","reference-count":19,"publisher":"Springer London","isbn-type":[{"value":"9783540197836","type":"print"},{"value":"9781447134213","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/978-1-4471-3421-3_14","type":"book-chapter","created":{"date-parts":[[2012,3,8]],"date-time":"2012-03-08T07:42:32Z","timestamp":1331192552000},"page":"253-262","source":"Crossref","is-referenced-by-count":6,"title":["Logic Programming via Proof-valued Computations"],"prefix":"10.1007","author":[{"given":"David J.","family":"Pym","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lincoln A.","family":"Wallen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","volume-title":"Implementing mathematics with the NuPRL proof development system","author":"RL Constable","year":"1986","unstructured":"R.L. Constable et al. Implementing mathematics with the NuPRL proof development system. Prentice Hall, 1986."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Linear logic. Theoret. Comput. Sci., 50(1), 1987.","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00247744","volume":"9","author":"K G\u00f6del","year":"1980","unstructured":"K. G\u00f6del. Uber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes, Dialectica, 12, 1958, pp.280\u2013287; English translation, J. Phil. Logic, 9, 1980, pp. 133\u2013142.","journal-title":"J. Phil. Logic"},{"key":"14_CR4","unstructured":"R. Harper, F. Honsell, G. Plotkin. A framework for defining logics. J. ACM, (to appear). (Preprint available as University of Edinburgh LFCS report ECS-LFCS-91\u2013162, June 1991.)"},{"key":"14_CR5","unstructured":"S.C. Kleene. Permutability of inferences in Gentzen\u2019s calculi LK and LJ. Mem. Amer. Math. Soc, pages 1\u201326, 1952."},{"key":"14_CR6","volume-title":"Mathematical Logic","author":"SC Kleene","year":"1968","unstructured":"S.C. Kleene. Mathematical Logic. Wiley and Sons, 1968."},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R Kowalski","year":"1971","unstructured":"R. Kowalski and D. Kuehner. Linear resolution with selection function. J. Ariif. Int., 2:227\u2013260, 1971.","journal-title":"J. Ariif. Int."},{"key":"14_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-96826-6","volume-title":"Foundations of Logic Programming","author":"J Lloyd","year":"1984","unstructured":"J. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984."},{"key":"14_CR9","volume-title":"Automated theorem proving: a logical basis","author":"DW Loveland","year":"1979","unstructured":"D.W. Loveland. Automated theorem proving: a logical basis. Elsevier, 1979."},{"key":"14_CR10","series-title":"Technical Report 2, Scuola di Specializziazione in Logica Matematica, Dipartimento di Matematica","volume-title":"On the meanings of the logical constants and the justifications of the logical laws","author":"P Martin-L\u00f6f","year":"1985","unstructured":"P. Martin-L\u00f6f. 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\u00e0 di Siena, 1985."},{"key":"14_CR11","series-title":"Report MS-CIS-86\u201317","volume-title":"Higher-order Logic Programming","author":"D Miller","year":"1986","unstructured":"D. Miller and G. Nadathur. Higher-order Logic Programming. Report MS-CIS-86\u201317, University of Pennsylvania, 1986."},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D Miller","year":"1991","unstructured":"D. Miller, G. Nadathur, A. Scedrov and F. Pfenning. Uniform Proofs as a Foundation for Logic Programming. Ann. Pure and Appl. Logic, 51, pp. 125\u2013157, 1991.","journal-title":"Ann. Pure and Appl. Logic"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1017\/CBO9780511569807.008","volume-title":"Logical Frameworks","author":"F Pfenning","year":"1991","unstructured":"F. Pfenning. Logic programming in the LF logical framework. In: Logical Frameworks, G. Huet and G. Plotkin (editors), Cambridge University Press, 1991. pp. 149\u2013181."},{"key":"14_CR14","volume-title":"Natural deduction: a proof-theoretical study","author":"D Prawitz","year":"1965","unstructured":"D. Prawitz. Natural deduction: a proof-theoretical study. Almqvist & Wiksell, 1965."},{"key":"14_CR15","first-page":"25","volume-title":"Essays on Mathematical and Philosophical Logic","author":"D Prawitz","year":"1978","unstructured":"D. Prawitz. Proofs and the meaning and completeness of the logical constants. In: J. Hintikka, I. Niiniluoto and E. Saarinen (eds.) Essays on Mathematical and Philosophical Logic, pp. 25\u201340. D. Reidel, 1978."},{"key":"14_CR16","volume-title":"Ph.D. thesis, University of Edinburgh","author":"DJ Pym","year":"1990","unstructured":"D.J. Pym. Proofs, Search and Computation in General Logic. Ph.D. thesis, University of Edinburgh, 1990. Available as report CST-69\u201390, Department of Computer Science, University of Edinburgh, 1990. (Also published as LFCS report ECS-LFCS-90\u2013125.)"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1017\/CBO9780511569807.013","volume-title":"Logical Frameworks","author":"DJ Pym","year":"1991","unstructured":"D.J. Pym and L.A. Wallen. Proof-search in the All-calculus. In: Logical Frameworks, G. Huet and G. Plotkin (editors), Cambridge University Press, 1991. pp. 309\u2013340."},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/BF01621477","volume":"30","author":"W Sieg","year":"1991","unstructured":"W. Sieg. Herbrand analyses. Arch. Math. Logic, 30, pp. 409\u2013441, 1991.","journal-title":"Arch. Math. Logic"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J Zucker","year":"1974","unstructured":"J. Zucker. The correspondence between cut-elimination and normalisation. Ann. Math. Logic, 7:1\u2013112, 1974.","journal-title":"Ann. Math. Logic"}],"container-title":["Workshops in Computing","ALPUK92"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3421-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T12:14:03Z","timestamp":1556453643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-3421-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540197836","9781447134213"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-3421-3_14","relation":{},"ISSN":["1431-1682"],"issn-type":[{"value":"1431-1682","type":"print"}],"subject":[],"published":{"date-parts":[[1993]]}}}