{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:54:13Z","timestamp":1725515653645},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_18","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"264-279","source":"Crossref","is-referenced-by-count":0,"title":["CDCL-Based Abstract State Transition System for Coherent Logic"],"prefix":"10.1007","author":[{"given":"Mladen","family":"Nikoli\u0107","sequence":"first","affiliation":[]},{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus as a First-Order DPLL Method. Artificial Intelligence\u00a0172(4-5) (2008)","DOI":"10.1016\/j.artint.2007.09.005"},{"key":"18_CR2","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/11591191_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Bezem","year":"2005","unstructured":"Bezem, M., Coquand, T.: Automating Coherent Logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 246\u2013260. Springer, Heidelberg (2005)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"M. Bezem. On the Undecidability of Coherent Logic. Processes, Terms and Cycles (2005)","DOI":"10.1007\/11601548_2"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Bezem, M., Hendriks, D.: On the Mechanization of the Proof of Hessenberg\u2019s Theorem in Coherent Logic. J. of Automated Reasoning\u00a040(1) (2008)","DOI":"10.1007\/s10817-007-9086-x"},{"key":"18_CR5","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (2009)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. J. of ACM 7(3) (1960)","DOI":"10.1145\/321033.321034"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-75292-9_14","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"J. Fisher","year":"2007","unstructured":"Fisher, J., Bezem, M.: Skolem Machines and Geometric Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 201\u2013215. Springer, Heidelberg (2007)"},{"key":"18_CR9","unstructured":"Jani\u010di\u0107, P., Kordi\u0107, S.: EUCLID \u2014 the geometry theorem prover. FILOMAT 9(3) (1995)"},{"key":"18_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A.: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 1\u201327. Springer, Heidelberg (2007)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Mari\u0107, F.: Formalization and Implementation of Modern SAT Solvers. J. of Automated Reasoning 43(1) (2009)","DOI":"10.1007\/s10817-009-9127-8"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Mari\u0107, F., Jani\u010di\u0107, P.: Formalization of Abstract State Transition Systems for SAT. Logical Methods in Computer Science 7(3) (2011)","DOI":"10.2168\/LMCS-7(3:19)2011"},{"key":"18_CR13","doi-asserted-by":"crossref","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. of ACM 53(6) (2006)","DOI":"10.1145\/1217856.1217859"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-02777-2_31","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M. Nikoli\u0107","year":"2009","unstructured":"Nikoli\u0107, M., Mari\u0107, F., Jani\u010di\u0107, P.: Instance-Based Selection of Policies for SAT Solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 326\u2013340. Springer, Heidelberg (2009)"},{"key":"18_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Automated Reasoning","author":"H. Nivelle de","year":"2006","unstructured":"de Nivelle, H., Meng, J.: Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 303\u2013317. Springer, Heidelberg (2006)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Piska\u010d, R., de Moura, L., Bjorner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. of Automated Reasoning 44 (2010)","DOI":"10.1007\/s10817-009-9161-6"},{"key":"18_CR17","unstructured":"Polonsky, A.: Proofs, Types, and Lambda Calculus. PhD thesis, University of Bergen (2010)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction in Geometry","author":"S. Stojanovi\u0107","year":"2011","unstructured":"Stojanovi\u0107, S., Pavlovi\u0107, V., Jani\u010di\u0107, P.: Automated Generation of Formal and Readable Proofs in Geometry Using Coherent Logic. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol.\u00a06877, Springer, Heidelberg (2011)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013183. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:28:46Z","timestamp":1556890126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}