乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,27]],"date-time":"2023-10-27T04:58:08Z","timestamp":1698382688233},"reference-count":53,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2001,3,2]],"date-time":"2001-03-02T00:00:00Z","timestamp":983491200000},"content-version":"vor","delay-in-days":791,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1999,1]]},"DOI":"10.1016\/s0304-3975(98)00244-8","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T19:40:02Z","timestamp":1049744402000},"page":"129-188","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"title":["Representing scope in intuitionistic deductions"],"prefix":"10.1016","volume":"211","author":[{"given":"Matthew","family":"Stone","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/S0304-3975(98)00244-8_BIB1","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/BF00881845","article-title":"Resolution theorem proving in reified modal logics","volume":"12","author":"Aitken","year":"1994","journal-title":"J. Automat. Reason."},{"issue":"3","key":"10.1016\/S0304-3975(98)00244-8_BIB2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"J. Logic Comput."},{"issue":"2","key":"10.1016\/S0304-3975(98)00244-8_BIB3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"J. Assoc. Comput. Mach."},{"issue":"3","key":"10.1016\/S0304-3975(98)00244-8_BIB4","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","article-title":"Modal theorem proving: an equational viewpoint","volume":"2","author":"Auffray","year":"1992","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB5","series-title":"Automated Theorem Proving","author":"Bibel","year":"1982"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB6","series-title":"Logics in AI","first-page":"262","article-title":"Tableau-based theorem proving and synthesis of \u03bb-terms in the intuitionistic logic","volume":"vol. 633","author":"Bittel","year":"1992"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB7","series-title":"Automated Deduction in Nonstandard Logics: Papers from the 1993 Fall Symp.","first-page":"9","article-title":"A tableau-based theorem proving method for intuitionistic logic","author":"Bittel","year":"1993"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB8","first-page":"101","article-title":"The sharing of structure in theorem-proving programs","volume":"7","author":"Boyer","year":"1972"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB9","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB10","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF00156916","article-title":"Are tableaux and improvement on truth-tables","volume":"1","author":"D'Agostino","year":"1992","journal-title":"J. Logic Language Inform."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB11","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/BF00881958","article-title":"A generalization of analytic deduction via labelled deductive systems. part I: Basic substructural logics","volume":"13","author":"D'Agostino","year":"1994","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB12","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","article-title":"The taming of the cut. classical refutations with analytic cut","volume":"4","author":"D'Agostino","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB13","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0304-3975(92)90290-V","article-title":"Multimodal logic programming using equational and order-sorted logic","volume":"105","author":"Debart","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB14","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","article-title":"Contraction-free sequent calculi for intuitionistic logic","volume":"57","author":"Dyckhoff","year":"1992","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB15","series-title":"Proc. 1989 Internat. Workshop on Extensions of Logic Programming","first-page":"157","article-title":"A logic program for transforming sequent proofs to natural deduction proofs","author":"Felty","year":"1991"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB16","series-title":"Intuitionistic Logic, Model Theory and Forcing","author":"Fitting","year":"1969"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB17","article-title":"Proof Methods for Modal and Intuitionistic Logics","volume":"vol. 169","author":"Fitting","year":"1983"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB18","first-page":"101","article-title":"A modal Herbrand theorem","volume":"28","author":"Fitting","year":"1996","journal-title":"Fund. Inform."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB19","series-title":"Logic for Computer Science: Foundations of Automated Theorem Proving","author":"Gallier","year":"1986"},{"issue":"2","key":"10.1016\/S0304-3975(98)00244-8_BIB20","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(93)90011-H","article-title":"Constructive logics. I. A tutorial on proof systems and typed \u03bb-calculi","volume":"110","author":"Gallier","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB21","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(94)00105-7","article-title":"On proof normalization in linear logic","volume":"135","author":"Galmiche","year":"1994","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/S0304-3975(98)00244-8_BIB22","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":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB23","series-title":"CSL 94","first-page":"61","article-title":"A \u03bb-caculus structure isomorphic to Gentzen-style sequent calculus structure","author":"Herbelin","year":"1994"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB24","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","first-page":"479","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB25","series-title":"Proc. IJCAI","first-page":"942","article-title":"A general proof method for first-order modal logic","author":"Jackson","year":"1987"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB26","series-title":"Two Papers on the Predicate Calculus","first-page":"1","article-title":"Permutation of inferences in Gentzen's calculi LK and LJ","author":"Kleene","year":"1951"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB27","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB28","series-title":"Formal Systems and Recursive Functions","first-page":"92","article-title":"Semantical analysis of intuitionistic logic","author":"Kripke","year":"1965"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB29","series-title":"LICS","first-page":"282","article-title":"Proof search in first-order linear logic and other cut-free sequent calculi","author":"Lincoln","year":"1994"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB30","first-page":"153","article-title":"Constructive mathematics and computer programming","volume":"vol. VI","author":"Martin-L\u00f6f","year":"1982"},{"issue":"1\u20132","key":"10.1016\/S0304-3975(98)00244-8_BIB31","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0743-1066(89)90031-9","article-title":"A logical analysis of modules in logic programming","volume":"6","author":"Miller","year":"1989","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB32","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","article-title":"Uniform proofs as a foundation for logic programming","volume":"51","author":"Miller","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB33","series-title":"Proc. Internat. Symp. on Logics Comput. Sci.","first-page":"272","article-title":"A multiple-conclusion meta-logic","author":"Miller","year":"1994"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB34","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF00881902","article-title":"A proof procedure for the logic of hereditary Harrop formulas","volume":"11","author":"Nadathur","year":"1993","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB35","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","article-title":"Semantics-based translation methods for modal logics","volume":"1","author":"Ohlbach","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB36","series-title":"Logic Programming and Automated Reasoning","first-page":"253","article-title":"Optimized translation of multi modal logic into predicate logic","volume":"vol. 698","author":"Ohlbach","year":"1993"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB37","series-title":"TABLEAUX 96","first-page":"244","article-title":"T-string-unification: unifying prefixes in non-classical proof methods","volume":"vol. 1071","author":"Otten","year":"1996"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB38","series-title":"Proc. 2nd Scand. Logic Symp., North-Holland","first-page":"235","article-title":"Ideas and results in proof theory","author":"Prawitz","year":"1971"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB39","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1093\/logcom\/1.4.537","article-title":"Some syntactical observations on linear logic","volume":"1","author":"Schellinx","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB40","series-title":"Automated Deduction: CADE 11","first-page":"522","article-title":"Proof search in the intuitionistic sequent calculus","author":"Shankar","year":"1992"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB41","article-title":"First-order Logic","volume":"vol. 43","author":"Smullyan","year":"1968"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB42","series-title":"Truth, Syntax and Modality","first-page":"274","article-title":"A generalization of intuitionistic and modal logics","author":"Smullyan","year":"1973"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB43","unstructured":"M. Stone, Efficient constraints on possible worlds for reasoning about necessity, Technical Report IRCS 97-7 and CIS 97-10, University of Pennsylvania."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB44","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF00885763","article-title":"Proof strategies in linear logic","volume":"12","author":"Tammet","year":"1994","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(98)00244-8_BIB45","article-title":"Autologic","author":"Tennant","year":"1992"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB46","volume":"vol. 1","author":"Troelstra","year":"1988"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB47","volume":"vol. 2","author":"Troelstra","year":"1988"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB48","doi-asserted-by":"crossref","first-page":"159","DOI":"10.2307\/2272955","article-title":"An intuitionistic completeness theorem for intuitionistic predicate logic","volume":"41","author":"Veldman","year":"1976","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB49","series-title":"TABLEAUX 96","first-page":"312","article-title":"Proof-search in intuitionistic logic based on constraint satisfaction","volume":"vol. 1071","author":"Voronkov","year":"1996"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB50","series-title":"Automated Proof Search in Non-Classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics","author":"Wallen","year":"1990"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB51","article-title":"Ein erweiterter intuitionistischer Sequenzenkalk\u00fcl und dessen Anwendung im intutitiotistischen Konnektionsbeweisen","author":"Schmitt","year":"1994"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB52","series-title":"Proc. Fourth Workshop on Theorem Proving with Analytic Tableaux and Related Methods","first-page":"106","article-title":"On transforming intuitionistic matrix proofs into standard-sequent proofs","volume":"volume 918","author":"Schmitt","year":"1995"},{"key":"10.1016\/S0304-3975(98)00244-8_BIB53","series-title":"Proc. Thirteenth International Conference on Automated Deduction","first-page":"418","article-title":"Converting non-classical matrix proofs into sequent-style systems","volume":"volume 1104","author":"Schmitt","year":"1996"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397598002448?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397598002448?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,10,26]],"date-time":"2023-10-26T12:07:50Z","timestamp":1698322070000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397598002448"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":53,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["S0304397598002448"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(98)00244-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1999,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Representing scope in intuitionistic deductions","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0304-3975(98)00244-8","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1999 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}