{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:27Z","timestamp":1725512007459},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_20","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T08:04:57Z","timestamp":1210061097000},"page":"211-224","source":"Crossref","is-referenced-by-count":16,"title":["SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions"],"prefix":"10.1007","author":[{"given":"Maarten","family":"Mari\u00ebn","sequence":"first","affiliation":[]},{"given":"Johan","family":"Wittocx","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Denecker","sequence":"additional","affiliation":[]},{"given":"Maurice","family":"Bruynooghe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"7","key":"20_CR1","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"20_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/3-540-44957-4_47","volume-title":"Computational Logic - CL 2000","author":"M. Denecker","year":"2000","unstructured":"Denecker, M.: Extending Classical Logic with Inductive Definitions. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 703\u2013717. Springer, Heidelberg (2000)"},{"key":"20_CR3","first-page":"365","volume-title":"LPNMR 1993","author":"M. Denecker","year":"1993","unstructured":"Denecker, M., De Schreye, D.: Justification semantics: A unifiying framework for the semantics of logic programs. In: LPNMR 1993, pp. 365\u2013379. MIT Press, Cambridge (1993)"},{"key":"20_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/978-3-540-24609-1_7","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Denecker","year":"2003","unstructured":"Denecker, M., Ternovska, E.: A Logic of Non-monotone Inductive Definitions and Its Modularity Properties. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol.\u00a02923, pp. 47\u201360. Springer, Heidelberg (2003)"},{"key":"20_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-72200-7_9","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Denecker","year":"2007","unstructured":"Denecker, M., Vennekens, J.: Well-Founded Semantics and the Algebraic Theory of Non-monotone Inductive Definitions. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol.\u00a04483, pp. 84\u201396. Springer, Heidelberg (2007)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"20_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-72200-7_23","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Gebser","year":"2007","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: A Conflict-Driven Answer Set Solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol.\u00a04483, pp. 260\u2013265. Springer, Heidelberg (2007)"},{"key":"20_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-72200-7_3","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Gebser","year":"2007","unstructured":"Gebser, M., Liu, L., Namasivayam, G., Neumann, A., Schaub, T., Truszczynski, M.: The First Answer Set Programming System Competition. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol.\u00a04483, pp. 3\u201317. Springer, Heidelberg (2007)"},{"issue":"1","key":"20_CR9","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0022-0000(93)90024-Q","volume":"47","author":"A. Gelder Van","year":"1993","unstructured":"Van Gelder, A.: The alternating fixpoint of logic programs with negation. Journal of Computer and System Sciences\u00a047(1), 185\u2013221 (1993)","journal-title":"Journal of Computer and System Sciences"},{"issue":"3","key":"20_CR10","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1145\/116825.116838","volume":"38","author":"A. Gelder Van","year":"1991","unstructured":"Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. J. ACM\u00a038(3), 620\u2013650 (1991)","journal-title":"J. ACM"},{"key":"20_CR11","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"20_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/11546207_44","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"Y. Lierler","year":"2005","unstructured":"Lierler, Y.: cmodels \u2013 SAT-Based Disjunctive Answer Set Solver. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol.\u00a03662, pp. 447\u2013451. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"20_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.artint.2004.04.004","volume":"157","author":"F. Lin","year":"2004","unstructured":"Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by sat solvers. Artif. Intell.\u00a0157(1-2), 115\u2013137 (2004)","journal-title":"Artif. Intell."},{"key":"20_CR14","series-title":"Lecture Notes in Artificial Intelligence","first-page":"673","volume-title":"Computational Logic - CL 2000","author":"Z. Lonc","year":"2000","unstructured":"Lonc, Z., Truszczy\u0144ski, M.: On the Problem of Computing the Well-Founded Semantics. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 673\u2013687. Springer, Heidelberg (2000)"},{"key":"20_CR15","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-642-60085-2_17","volume-title":"The Logic Programming Paradigm: a 25-Year Perspective","author":"V.W. Marek","year":"1999","unstructured":"Marek, V.W., Truszczy\u0144ski, M.: Stable models and an alternative logic programming paradigm. In: The Logic Programming Paradigm: a 25-Year Perspective, pp. 375\u2013398. Springer, Heidelberg (1999)"},{"key":"20_CR16","unstructured":"Mari\u00ebn, M., Wittocx, J., Denecker, M.: The IDP framework for declarative problem solving. In: Search and Logic: Answer Set Programming and SAT, pp. 19\u201334 (2006)"},{"key":"20_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-75560-9_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Mari\u00ebn","year":"2007","unstructured":"Mari\u00ebn, M., Wittocx, J., Denecker, M.: Integrating Inductive Definitions in SAT. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 378\u2013392. Springer, Heidelberg (2007)"},{"key":"20_CR18","unstructured":"Mari\u00ebn, M., Wittocx, J., Denecker, M.: MidL: a SAT(ID) solver. In: 4th Workshop on Answer Set Programming: Advances in Theory and Implementation, pp. 303\u2013308 (2007)"},{"key":"20_CR19","unstructured":"MiniSat(ID), \n \n http:\/\/www.cs.kuleuven.be\/~dtai\/krr\/software\/minisatid.html"},{"key":"20_CR20","unstructured":"Mitchell, D.G., Ternovska, E.: A framework for representing and solving NP search problems. In: AAAI 2005, pp. 430\u2013435. AAAI Press \/ The MIT Press (2005)"},{"key":"20_CR21","first-page":"530","volume-title":"DAC 2001","author":"M. Moskewicz","year":"2001","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC 2001, pp. 530\u2013535. ACM Press, New York (2001)"},{"issue":"6","key":"20_CR22","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\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(t). J. ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11562931_18","volume-title":"Logic Programming","author":"N. Pelov","year":"2005","unstructured":"Pelov, N., Ternovska, E.: Reducing Inductive Definitions to Propositional Satisfiability. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 221\u2013234. Springer, Heidelberg (2005)"},{"issue":"5","key":"20_CR24","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P.M. Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"key":"20_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/978-3-540-24609-1_26","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"J. Ward","year":"2003","unstructured":"Ward, J., Schlipf, J.S.: Answer Set Programming with Clause Learning. In: Lifschitz, V., Niemel\u00e4, I. (eds.) LPNMR 2004. LNCS (LNAI), vol.\u00a02923, pp. 302\u2013313. Springer, Heidelberg (2003)"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/11799573_19","volume-title":"Logic Programming","author":"J. Wittocx","year":"2006","unstructured":"Wittocx, J., Vennekens, J., Mari\u00ebn, M., Denecker, M., Bruynooghe, M.: Predicate Introduction Under Stable and Well-Founded Semantics. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol.\u00a04079, pp. 242\u2013256. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:29:13Z","timestamp":1619522953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_20","relation":{},"subject":[]}}