{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T03:58:54Z","timestamp":1649044734921},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf01531029","type":"journal-article","created":{"date-parts":[[2005,4,19]],"date-time":"2005-04-19T00:21:39Z","timestamp":1113870099000},"page":"201-234","source":"Crossref","is-referenced-by-count":0,"title":["The expected complexity of analytic tableaux analyses in propositional calculus ? II"],"prefix":"10.1007","volume":"6","author":[{"given":"John W.","family":"Rosenthal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1137\/1016082","volume":"16","author":"E.A. Bender","year":"1974","unstructured":"E.A. Bender, Asymptotic methods in enumeration, SIAM Rev. 16 (1974) 485?515.","journal-title":"SIAM Rev."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1137\/0210043","volume":"10","author":"C. Brown","year":"1981","unstructured":"C. Brown and P. Purdom Jr., An average time analysis of backtracking, Siam J. Comput. 10 (1981) 583?593.","journal-title":"Siam J. Comput."},{"key":"CR3","unstructured":"M. Chao and J. Franco, Probabilistic analysis of the unit clause and maximum occurring literal selection heuristics for the 3-satisfiability problem, preprint."},{"key":"CR4","unstructured":"M. Chao and J. Franco, Probabilistic analysis of a generalization of the unit clause literal selection heuristic for thek-satisfiability problem, preprint."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF01874393","volume":"1","author":"J. Franco","year":"1984","unstructured":"J. Franco, Probabilistic analysis of the pure literal heuristic for the satisfiability problem, Ann. Oper. Res. 1 (1984) 273?289.","journal-title":"Ann. Oper. Res."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","volume":"5","author":"J. Franco","year":"1983","unstructured":"J. Franco and M. Paull, Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem, Discr. Appl. Math. 5 (1983) 77?87.","journal-title":"Discr. Appl. Math."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/0166-218X(87)90032-1","volume":"17","author":"J. Franco","year":"1987","unstructured":"J. Franco, J. Plotkin and J. Rosenthal, Correction to probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem, Discr. Appl. Math. 17 (1987) 295?299.","journal-title":"Discr. Appl. Math."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/0020-0190(82)90110-7","volume":"15","author":"A. Goldberg","year":"1982","unstructured":"A. Goldberg, P. Purdom and C. Brown, Average time analysis of simplified Davis-Putnam procedures, Inform. Proc. Lett. 15 (1982) 72?75.","journal-title":"Inform. Proc. Lett."},{"key":"CR9","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0020-0190(83)90127-8","volume":"16","author":"A. Goldberg","year":"1983","unstructured":"A. Goldberg, P. Purdom and C. Brown, Corrigendum average time analysis of simplified Davis-Putnam procedures, Inform. Proc. Lett. 16 (1983) 213.","journal-title":"Inform. Proc. Lett."},{"key":"CR10","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1215\/S0012-7094-58-02504-3","volume":"25","author":"L. Moser","year":"1958","unstructured":"L. Moser and M. Wyman, Stirling numbers of the second kind, Duke Math. J. 25 (1958) 29?43.","journal-title":"Duke Math. J."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1305\/ndjfl\/1093870153","volume":"23","author":"J.M. Plotkin","year":"1982","unstructured":"J.M. Plotkin and J.W. Rosenthal, the expected complexity of analytic tableaux analyses in propositional calculus, Notre Dame J. Formal Logic 23 (1982) 409?426.","journal-title":"Notre Dame J. Formal Logic"},{"key":"CR12","unstructured":"J.M. Plotkin and J.W. Rosenthal, The probability of pure literals, submitted to Ann. Oper. Res."},{"key":"CR13","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1137\/0212049","volume":"12","author":"P. Purdom Jr.","year":"1983","unstructured":"P. Purdom Jr. and C. Brown, An analysis of backtracking with search rearrangement, Siam J. Comput. 12 (1983) 717?733.","journal-title":"Siam J. Comput."},{"key":"CR14","volume-title":"Combinatorial Identities","author":"J. Riordan","year":"1968","unstructured":"J. Riordan,Combinatorial Identities (Wiley, New York, 1968)."},{"key":"CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R. Smullyan","year":"1968","unstructured":"R. Smullyan,First Order Logic (Springer, New York, 1968)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01531029\/fulltext.html","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01531029.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01531029\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01531029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:31:34Z","timestamp":1556890294000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01531029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":15,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01531029"],"URL":"https:\/\/doi.org\/10.1007\/bf01531029","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}