{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,6]],"date-time":"2022-12-06T14:21:25Z","timestamp":1670336485082},"reference-count":11,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3850,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1016\/s0304-3975(02)00079-8","type":"journal-article","created":{"date-parts":[[2002,10,28]],"date-time":"2002-10-28T17:15:47Z","timestamp":1035825347000},"page":"1107-1113","source":"Crossref","is-referenced-by-count":2,"title":["A syntactical proof of the Marriage Lemma"],"prefix":"10.1016","volume":"290","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(02)00079-8_BIB1","doi-asserted-by":"crossref","unstructured":"P. Beame, T. Pitassi, Simplified and improved resolution lower bounds, Proc. of FOCS\u201986.","DOI":"10.1109\/SFCS.1996.548486"},{"key":"10.1016\/S0304-3975(02)00079-8_BIB2","doi-asserted-by":"crossref","unstructured":"J. Cederquist, Th. Coquand, Entailment relations and distributive lattices, Proc. of Logic Colloquium 98, Prague, Lect. Notes Log. 13, Assoc. Symbol. Logic, Urbana, IL, 2000, pp. 127\u2013139.","DOI":"10.1017\/9781316756140.011"},{"key":"10.1016\/S0304-3975(02)00079-8_BIB3","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0022-4049(99)00095-X","article-title":"Valuations and Dedekind Prague theorem","volume":"155","author":"Coquand","year":"2001","journal-title":"J. Pure Appl. Algebra"},{"key":"10.1016\/S0304-3975(02)00079-8_BIB4","series-title":"CSL2000","first-page":"277","article-title":"Sequents, frame and completness","volume":"Vol. 1862","author":"Coquand","year":"2000"},{"key":"10.1016\/S0304-3975(02)00079-8_BIB5","doi-asserted-by":"crossref","first-page":"214","DOI":"10.2307\/2372148","article-title":"The marriage problem","volume":"72","author":"Halmos","year":"1950","journal-title":"Amer. J. Math."},{"key":"10.1016\/S0304-3975(02)00079-8_BIB6","doi-asserted-by":"crossref","unstructured":"V. Lifschitz, Semantical completeness theorem in logic and algebra, Proc. Amer. Math. Soc., Vol. 79, 1980, pp. 89\u201396.","DOI":"10.1090\/S0002-9939-1980-0560591-4"},{"key":"10.1016\/S0304-3975(02)00079-8_BIB7","unstructured":"Y. Matiyasevich, Proof Procedures as Bases for Metamathematical Proofs in Discrete Mathematics. Available on the web address http:\/\/logic.pdmi.ras.ru\/yumat\/journal\/jcontord.htm."},{"key":"10.1016\/S0304-3975(02)00079-8_BIB8","doi-asserted-by":"crossref","first-page":"521","DOI":"10.2307\/2308219","article-title":"The problem of simplifying truth functions","volume":"59","author":"Quine","year":"1952","journal-title":"Am. Meth. Monthly"},{"key":"10.1016\/S0304-3975(02)00079-8_BIB9","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1112\/jlms\/s1-42.1.321","article-title":"Note on the transfinite case of Hall's theorem on representatives","volume":"42","author":"Rado","year":"1967","journal-title":"J. London Math. Soc."},{"key":"10.1016\/S0304-3975(02)00079-8_BIB10","first-page":"77","article-title":"The generalised resolution principle","volume":"3","author":"Robinson","year":"1968","journal-title":"Mach. Intell."},{"key":"10.1016\/S0304-3975(02)00079-8_BIB11","doi-asserted-by":"crossref","unstructured":"D. Scott, Completeness and axiomatizability, Proc. Tarski Sympos., 1974, pp. 411\u2013435.","DOI":"10.1090\/pspum\/025\/0363802"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502000798?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502000798?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T07:55:58Z","timestamp":1578470158000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397502000798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":11,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["S0304397502000798"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(02)00079-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}