{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:46:25Z","timestamp":1743065185201,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642415234"},{"type":"electronic","value":"9783642415241"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41524-1_17","type":"book-chapter","created":{"date-parts":[[2013,11,15]],"date-time":"2013-11-15T10:48:20Z","timestamp":1384512500000},"page":"289-296","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Computing with Logic as Operator Elimination: The ToyElim System"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,11,16]]},"reference":[{"key":"17_CR1","volume-title":"Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications","author":"DM Gabbay","year":"2008","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, London (2008)"},{"key":"17_CR2","unstructured":"Huang, J., Darwiche, A.: DPLL with a trace: from SAT to knowledge compilation. In: IJCAI-05, pp. 156\u2013162. Morgan Kaufmann (2005)"},{"issue":"6","key":"17_CR3","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1093\/logcom\/2.6.719","volume":"2","author":"AC Kakas","year":"1993","unstructured":"Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive logic programming. J. Logic Comput. 2(6), 719\u2013770 (1993)","journal-title":"J. Logic Comput."},{"key":"17_CR4","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 - formula-variable independence and forgetting. J. Artif. Intell. Res. 18, 391\u2013443 (2003)","journal-title":"J. Artif. Intell. Res."},{"key":"17_CR5","first-page":"298","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"V Lifschitz","year":"1994","unstructured":"Lifschitz, V.: Circumscription. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 298\u2013352. Oxford University Press, Oxford (1994)"},{"key":"17_CR6","first-page":"37","volume-title":"ICLP 2008. LNCS","author":"V Lifschitz","year":"2008","unstructured":"Lifschitz, V.: Twelve definitions of a stable model. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"17_CR7","unstructured":"Lin, F.: A study of nonmonotonic reasoning. Ph.D. thesis, Stanford University (1991)"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/S0004-3702(01)00070-4","volume":"128","author":"F Lin","year":"2001","unstructured":"Lin, F.: On strongest necessary and weakest sufficient conditions. Artif. Intell. 128, 143\u2013159 (2001)","journal-title":"Artif. Intell."},{"key":"17_CR9","first-page":"436","volume-title":"SAT 2012. LNCS","author":"N Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436\u2013441. Springer, Heidelberg (2012)"},{"key":"17_CR10","first-page":"165","volume-title":"TABLEAUX 2003. LNCS (LNAI)","author":"NV Murray","year":"2003","unstructured":"Murray, N.V., Rosenthal, E.: Tableaux, path dissolution and decomposable negation normal form for knowledge compilation. In: Mayer, M.C., Pirri, F. (eds.) TABLEAUX 2003. LNCS (LNAI), vol. 2796, pp. 165\u2013180. Springer, Heidelberg (2003)"},{"key":"17_CR11","first-page":"389","volume-title":"JELIA 2008. LNCS (LNAI)","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. 5293, pp. 389\u2013402. Springer, Heidelberg (2008)"},{"key":"17_CR12","first-page":"325","volume-title":"TABLEAUX 2009. LNCS","author":"C Wernhard","year":"2009","unstructured":"Wernhard, C.: Tableaux for projection computation and knowledge compilation. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 325\u2013340. Springer, Heidelberg (2009)"},{"key":"17_CR13","unstructured":"Wernhard, C.: Circumscription and projection as primitives of logic programming. In: Technical Communications of the ICLP 2010. LIPIcs, vol. 7, pp. 202\u2013211 (2010)"},{"key":"17_CR14","unstructured":"Wernhard, C.: Forward human reasoning modeled by logic programming modeled by classical logic with circumscription and projection. Technical Report Knowledge Representation and Reasoning 11-07, Technische Universit\u00e4t Dresden (2011)"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"1089","DOI":"10.1016\/j.jsc.2011.12.034","volume":"47","author":"C Wernhard","year":"2012","unstructured":"Wernhard, C.: Projection and scope-determined circumscription. J. Symb. Comput. 47, 1089\u20131108 (2012)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Applications of Declarative Programming and Knowledge Management"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41524-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T19:20:15Z","timestamp":1675797615000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-41524-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415234","9783642415241"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41524-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"16 November 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}