{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:28Z","timestamp":1725533848514},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027154"},{"type":"electronic","value":"9783642027161"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02716-1_24","type":"book-chapter","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T04:22:21Z","timestamp":1246335741000},"page":"325-340","source":"Crossref","is-referenced-by-count":3,"title":["Tableaux for Projection Computation and Knowledge Compilation"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Or\u0142owska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS(LNAI), vol.\u00a01126, pp. 1\u201317. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61630-6_1"},{"key":"24_CR2","unstructured":"Bayardo, R.J., Pehoushek, J.D.: Counting models using connected components. In: AAAI-2000, pp. 157\u2013162 (2000)"},{"issue":"1","key":"24_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F. Bry","year":"2000","unstructured":"Bry, F., Yahya, A.H.: Positive unit hyperresolution tableaux and their application to minimal model generation. J. Autom. Reason.\u00a025(1), 35\u201382 (2000)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A. Darwiche","year":"2001","unstructured":"Darwiche, A.: Decomposable negation normal form. JACM\u00a048(4), 608\u2013647 (2001)","journal-title":"JACM"},{"key":"24_CR5","unstructured":"Darwiche, A.: New advances in compiling CNF to decomposable negation normal form. In: ECAI 2004, pp. 328\u2013332 (2004)"},{"key":"24_CR6","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A. Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. JAIR\u00a017, 229\u2013264 (2002)","journal-title":"JAIR"},{"key":"24_CR7","first-page":"537","volume-title":"Handbook of Automated Reasoning","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Handbook of Automated Reasoning, vol.\u00a0I, ch. 1, pp. 537\u2013610. Elsevier Science, Amsterdam (2001)"},{"key":"24_CR8","unstructured":"Ebbinghaus, H.-D., Flum, J., Thomas, W.: Einf\u00fchrung in die mathematische Logik, 4th edn. Spektrum Akademischer Verlag, Heidelberg (1996)"},{"key":"24_CR9","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications (2008)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/11425274_32","volume-title":"Foundations of Intelligent Systems","author":"R. H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R., Murray, N.V., Rosenthal, E.: Normal forms for knowledge compilation. In: Hacid, M.-S., Murray, N.V., Ra\u015b, Z.W., Tsumoto, S. (eds.) ISMIS 2005. LNCS, vol.\u00a03488, pp. 304\u2013313. Springer, Heidelberg (2005)"},{"key":"24_CR11","unstructured":"Huang, J., Darwiche, A.: DPLL with a trace: From SAT to knowledge compilation. In: IJCAI 2005, pp. 156\u2013162 (2005)"},{"issue":"5","key":"24_CR12","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/9.5.651","volume":"9","author":"J. Kohlas","year":"1999","unstructured":"Kohlas, J., Haenni, R., Moral, S.: Propositional information systems. J. Logic and Comp.\u00a09(5), 651\u2013681 (1999)","journal-title":"J. Logic and Comp."},{"key":"24_CR13","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1613\/jair.1113","volume":"18","author":"J. Lang","year":"2003","unstructured":"Lang, J., Liberatore, P., Marquis, P.: Propositional independence \u2013 formula-variable independence and forgetting. JAIR\u00a018, 391\u2013443 (2003)","journal-title":"JAIR"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"issue":"3","key":"24_CR15","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/174130.174135","volume":"40","author":"N.V. Murray","year":"1993","unstructured":"Murray, N.V., Rosenthal, E.: Dissolution: Making paths vanish. JACM\u00a040(3), 504\u2013535 (1993)","journal-title":"JACM"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-540-45206-5_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"N.V. Murray","year":"2003","unstructured":"Murray, N.V., Rosenthal, E.: Tableaux, path dissolution and decomposable negation normal form for knowledge compilation. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol.\u00a02796, pp. 165\u2013180. Springer, Heidelberg (2003)"},{"issue":"6","key":"24_CR17","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). JACM\u00a053(6), 937\u2013977 (2006)","journal-title":"JACM"},{"key":"24_CR18","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/978-3-540-30227-8_46","volume-title":"Logics in Artificial Intelligence","author":"C. Wernhard","year":"2004","unstructured":"Wernhard, C.: Semantic knowledge partitioning. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 552\u2013564. Springer, Heidelberg (2004)"},{"key":"24_CR19","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-540-87803-2_32","volume-title":"Logics in Artificial Intelligence","author":"C. Wernhard","year":"2008","unstructured":"Wernhard, C.: Literal projection for first-order logic. In: H\u00f6lldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol.\u00a05293, pp. 389\u2013402. Springer, Heidelberg (2008)"},{"key":"24_CR20","unstructured":"Wernhard, C.: Automated Deduction for Projection Elimination. Dissertationen zur K\u00fcnstlichen Intelligenz (DISKI), vol.\u00a0324. AKA\/IOS Press (2009)"}],"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\/978-3-642-02716-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:26:28Z","timestamp":1606184788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02716-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027154","9783642027161"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02716-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}