{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:39Z","timestamp":1725475899941},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_3","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"40-51","source":"Crossref","is-referenced-by-count":5,"title":["Local Symmetries in Propositional Logic"],"prefix":"10.1007","author":[{"given":"Noriko H.","family":"Arai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alasdair","family":"Urquhart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Arai, N.H.: No feasible monotone interpolation for cut-free Gentzen type propositional calculus with permutation inference. Forthcoming, Theoretical Computer Science"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Arai, N.H.: Tractability of cut-free gentzen type propositional calculus with permutation inference II. Theoretical Computer Science (Forthcoming)","DOI":"10.1016\/S0304-3975(98)00186-8"},{"key":"3_CR3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0304-3975(96)80704-3","volume":"170","author":"N.H. Arai","year":"1996","unstructured":"Arai, N.H.: Tractability of cut-free gentzen type propositional calculus with permutation inference. Theoretical Computer Science\u00a0170, 129\u2013144 (1996)","journal-title":"Theoretical Computer Science"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow -resolution made simple. In: Proceedings of the 31st Annual ACM Symposium on Theory of Computing, pp. 517\u2013526 (1999)","DOI":"10.1145\/301250.301392"},{"key":"3_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9967-7","volume-title":"Graph Theory","author":"B. Bollob\u00e1s","year":"1979","unstructured":"Bollob\u00e1s, B.: Graph Theory. Springer, Heidelberg (1979)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Boppana, R., Sipser, M.: The complexity of finite functions. In: Handbook of Theoretical Computer Science. Algorithms and Complexity, vol.\u00a0A, pp. 757\u2013804. MIT Press\/Elsevier (1990)","DOI":"10.1016\/B978-0-444-88071-0.50019-9"},{"key":"3_CR7","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. Journal of the Association for Computing Machinery\u00a035, 759\u2013768 (1988)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting plane proofs. Discrete Applied Mathematics\u00a018, 25\u201338 (1987)","journal-title":"Discrete Applied Mathematics"},{"key":"3_CR9","first-page":"269","volume-title":"Recent advances in mathematical programming","author":"R.E. Gomory","year":"1963","unstructured":"Gomory, R.E.: An algorithm for integer solutions of linear programs. In: Graves, R.L., Wolfe, P. (eds.) Recent advances in mathematical programming, pp. 269\u2013302. McGraw-Hill, New York (1963)"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"3_CR11","volume-title":"Introduction to switching and automata theory","author":"M.A. Harrison","year":"1965","unstructured":"Harrison, M.A.: Introduction to switching and automata theory. McGraw-Hill Book Company, New York (1965)"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B. Krishnamurthy","year":"1985","unstructured":"Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica\u00a022, 253\u2013275 (1985)","journal-title":"Acta Informatica"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic\u00a062, 981\u2013998 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"#cr-split#-3_CR14.1","unstructured":"Razborov, A.A.: Lower bounds on the monotone complexity of some Boo- lean functions. Doklady Akademii Nauk SSSR\u00a0281, 798\u2013801 (1985);"},{"key":"#cr-split#-3_CR14.2","unstructured":"English translation. Soviet Mathematics, Doklady 31, 354\u2013357 (1985)"},{"key":"3_CR15","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the Association for Computing Machinery\u00a034, 209\u2013219 (1987)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0166-218X(99)00039-6","volume":"96-97","author":"A. Urquhart","year":"1999","unstructured":"Urquhart, A.: The symmetry rule in propositional logic. Discrete Applied Mathematics\u00a096-97, 177\u2013193 (1999)","journal-title":"Discrete Applied Mathematics"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:47:10Z","timestamp":1556020030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10722086_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}