{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:47:29Z","timestamp":1771890449320,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540878025","type":"print"},{"value":"9783540878032","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87803-2_32","type":"book-chapter","created":{"date-parts":[[2008,9,23]],"date-time":"2008-09-23T10:35:16Z","timestamp":1222166116000},"page":"389-402","source":"Crossref","is-referenced-by-count":5,"title":["Literal Projection for First-Order Logic"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR 1992, pp. 425\u2013435 (1992)"},{"key":"32_CR2","unstructured":"Lin, F., Reiter, R.: Forget It! In: Working Notes, AAAI Fall Symposium on Relevance, pp. 154\u2013159 (1994)"},{"issue":"3","key":"32_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1005722130532","volume":"18","author":"P. Doherty","year":"1997","unstructured":"Doherty, P., \u0141ukaszewicz, W., Sza\u0142as, A.: Computing circumscription revisited: A reduction algorithm. J. Autom. Reason.\u00a018(3), 297\u2013338 (1997)","journal-title":"J. Autom. Reason."},{"key":"32_CR4","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":"4","key":"32_CR5","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":"32_CR6","series-title":"Lecture Notes in Artificial Intelligence","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.A. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 552\u2013564. Springer, Heidelberg (2004)"},{"key":"32_CR7","unstructured":"Ghilardi, S., Lutz, C., Wolter, F.: Did I damage my ontology? A case for conservative extensions in description logics. In: KR 2006, pp. 187\u2013197 (2006)"},{"key":"32_CR8","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications (2008)"},{"issue":"1-5","key":"32_CR9","first-page":"1","volume":"2","author":"W. Conradie","year":"2006","unstructured":"Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic. I. the core algorithm SQEMA. Log. Meth. in Comp. Science\u00a02(1-5), 1\u201326 (2006)","journal-title":"Log. Meth. in Comp. Science"},{"key":"32_CR10","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)"},{"key":"32_CR11","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 \u2014 formula-variable independence and forgetting. JAIR\u00a018, 391\u2013443 (2003)","journal-title":"JAIR"},{"key":"32_CR12","unstructured":"Wernhard, C.: Automated Deduction for Projection Elimination. PhD thesis, Universit\u00e4t Koblenz-Landau, Germany (to appear, 2008)"},{"issue":"1-2","key":"32_CR13","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reason.\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Autom. Reason."},{"key":"32_CR14","volume-title":"Einf\u00fchrung in die mathematische Logik","author":"H.D. Ebbinghaus","year":"1996","unstructured":"Ebbinghaus, H.D., Flum, J., Thomas, W.: Einf\u00fchrung in die mathematische Logik, 4th edn. Spektrum Akademischer Verlag, Heidelberg (1996)","edition":"4"},{"key":"32_CR15","unstructured":"Huang, J., Darwiche, A.: DPLL with a trace: From SAT to knowledge compilation. In: IJCAI 2005, pp. 156\u2013162 (2005)"},{"key":"32_CR16","unstructured":"Wernhard, C.: Literal projection for first-order logic (extended version). Technical Report Fachbereich Informatik, Universit\u00e4t Koblenz-Landau (to appear, 2008)"},{"key":"32_CR17","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/BF01448035","volume":"110","author":"W. Ackermann","year":"1935","unstructured":"Ackermann, W.: Untersuchungen \u00fcber das Eliminationsproblem der mathematischen Logik. Math. Annalen\u00a0110, 390\u2013413 (1935)","journal-title":"Math. Annalen"},{"issue":"6","key":"32_CR18","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1093\/logcom\/3.6.605","volume":"3","author":"A. Szalas","year":"1993","unstructured":"Szalas, A.: On the correspondence between modal and classical logic: An automated approach. J. Log. Comput.\u00a03(6), 605\u2013620 (1993)","journal-title":"J. Log. Comput."},{"key":"32_CR19","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, pp. 537\u2013610. Elsevier, Amsterdam (2001)"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87803-2_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:49:58Z","timestamp":1619524198000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87803-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540878025","9783540878032"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87803-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}