乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T05:18:19Z","timestamp":1735708699895,"version":"3.32.0"},"reference-count":35,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4958,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2000]]},"DOI":"10.1016\/s1571-0661(05)01132-1","type":"journal-article","created":{"date-parts":[[2005,4,8]],"date-time":"2005-04-08T13:19:45Z","timestamp":1112966385000},"page":"1-18","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Notes Towards a Semantics for Proof-search"],"prefix":"10.1016","volume":"37","author":[{"given":"David J.","family":"Pym","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)01132-1_bib1","first-page":"118","article-title":"\u03bb-calculi with types","volume":"Volume 2","author":"Barendregt","year":"1992"},{"key":"10.1016\/S1571-0661(05)01132-1_bib2","series-title":"\u201cLogic, Logic, and Logic\u201d","first-page":"365","article-title":"Don't eliminate cut","author":"Boolos","year":"1998"},{"year":"1986","series-title":"\u201cLogic and Structure\u201d","author":"van Dalen","key":"10.1016\/S1571-0661(05)01132-1_bib3"},{"year":"1980","series-title":"\u201cElements of Intuitionism\u201d","author":"Dummett","key":"10.1016\/S1571-0661(05)01132-1_bib4"},{"issue":"4","key":"10.1016\/S1571-0661(05)01132-1_bib5","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/321978.321991","article-title":"The Semantics of Predicate Logic as a Programming Language","volume":"23","author":"van Emden","year":"1976","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0661(05)01132-1_bib6","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0304-3975(99)00169-3","article-title":"Proof-search in type-theoretic languages: an introduction","volume":"232","author":"Galmiche","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)01132-1_bib7","first-page":"405","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"176\u2013210","author":"Gentzen","year":"1934","journal-title":"Math. Zeit."},{"year":"1996","series-title":"\u201cArtificial intelligence and scientific method\u201d","author":"Gillies","key":"10.1016\/S1571-0661(05)01132-1_bib8"},{"key":"10.1016\/S1571-0661(05)01132-1_bib9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear Logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)01132-1_bib10","first-page":"391","article-title":"Resource-distribution via Boolean (extended abstract)","volume":"1249","author":"Harland","year":"1997","journal-title":"LNCS"},{"key":"10.1016\/S1571-0661(05)01132-1_bib11","unstructured":"Harland, J., D. Pym and M. Winikoff, Forward and Backward Chaining in Linear Logic (Extended Abstract), this volume."},{"key":"10.1016\/S1571-0661(05)01132-1_bib12","series-title":"\u201cTo H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism\u201d","first-page":"480","article-title":"The propositions-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/S1571-0661(05)01132-1_bib13","unstructured":"Ishtiaq, S., \u201cA Relevant Analysis of Natural Deduction\u201d, Ph.D. thesis, Department of Computer Science, Queen Mary and Westfield College, University of London, 1999."},{"issue":"6","key":"10.1016\/S1571-0661(05)01132-1_bib14","doi-asserted-by":"crossref","first-page":"809","DOI":"10.1093\/logcom\/8.6.809","article-title":"A Relevant Analysis of Natural Deduction","volume":"8","author":"Ishtiaq","year":"1998","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1571-0661(05)01132-1_bib15","first-page":"235","article-title":"Kripke resource models of a dependently-typed, bunched \u03bb-calculus (Extended Abstract)","volume":"1683","author":"Ishtiaq","year":"1999","journal-title":"LNCS"},{"author":"Ishtiaq","key":"10.1016\/S1571-0661(05)01132-1_bib16"},{"year":"1998","series-title":"\u201cCategorical Logic and Type Theory\u201d","author":"Jacobs","key":"10.1016\/S1571-0661(05)01132-1_bib17"},{"year":"1968","series-title":"\u201cMathematical Logic\u201d","author":"Kleene","key":"10.1016\/S1571-0661(05)01132-1_bib18"},{"year":"1986","series-title":"\u201cIntroduction to Higher-Order Categorical Logic\u201d","author":"Lambek","key":"10.1016\/S1571-0661(05)01132-1_bib19"},{"year":"1971","series-title":"Categories for the Working Mathematician","author":"Mac Lane","key":"10.1016\/S1571-0661(05)01132-1_bib20"},{"issue":"2","key":"10.1016\/S1571-0661(05)01132-1_bib21","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","article-title":"The Logic of Bunched Implications","volume":"5","author":"O'Hearn","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.1016\/S1571-0661(05)01132-1_bib22","first-page":"190","article-title":"\u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction","volume":"624","author":"Parigot","year":"1992","journal-title":"LNCS"},{"key":"10.1016\/S1571-0661(05)01132-1_bib23","doi-asserted-by":"crossref","unstructured":"Pym, D., On Bunched Predicate Logic, Proc. 14th LICS 1999, IEEE Computer Society Press, 183\u2013192.","DOI":"10.1109\/LICS.1999.782614"},{"author":"Pym","key":"10.1016\/S1571-0661(05)01132-1_bib24"},{"author":"Pym","key":"10.1016\/S1571-0661(05)01132-1_bib25"},{"author":"Pym","key":"10.1016\/S1571-0661(05)01132-1_bib26"},{"key":"10.1016\/S1571-0661(05)01132-1_bib27","doi-asserted-by":"crossref","unstructured":"Pym, D. and E. Ritter, A Semantics for Proof-search, manuscript, September 2000.","DOI":"10.1016\/S1571-0661(05)01132-1"},{"key":"10.1016\/S1571-0661(05)01132-1_bib28","series-title":"\u201cLogical Frameworks\u201d","first-page":"309","article-title":"Proof-search in the \u03bbII-calculus","author":"Pym","year":"1991"},{"key":"10.1016\/S1571-0661(05)01132-1_bib29","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0304-3975(99)00178-4","article-title":"On the intuitionistic force of classical search","volume":"232","author":"Ritter","year":"2000","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(05)01132-1_bib30","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/10.2.173","article-title":"Proof-terms for Classical and Intuitionistic Resolution","volume":"10","author":"Ritter","year":"2000","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1571-0661(05)01132-1_bib31","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the Association for Computing Machinery"},{"year":"1986","series-title":"\u201cDenotational Semantics\u201d","author":"Schmidt","key":"10.1016\/S1571-0661(05)01132-1_bib32"},{"year":"1994","series-title":"\u201cThe Art of Prolog\u201d","author":"Sterling","key":"10.1016\/S1571-0661(05)01132-1_bib33"},{"year":"1996","series-title":"\u201cBasic Proof Theory\u201d","author":"Troelstra","key":"10.1016\/S1571-0661(05)01132-1_bib34"},{"year":"1990","series-title":"\u201cAutomated Deduction in Non-Classical Logics\u201d","author":"Wallen","key":"10.1016\/S1571-0661(05)01132-1_bib35"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011321?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011321?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,31]],"date-time":"2024-12-31T09:56:28Z","timestamp":1735638988000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105011321"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"references-count":35,"alternative-id":["S1571066105011321"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)01132-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2000]]}}}