{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T21:03:01Z","timestamp":1791061381789,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642331244","type":"print"},{"value":"9783642331251","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_23","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T02:47:24Z","timestamp":1346208444000},"page":"334-351","source":"Crossref","is-referenced-by-count":22,"title":["A Generalization of St\u00e5lmarck\u2019s Method"],"prefix":"10.1007","author":[{"given":"Aditya","family":"Thakur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s10817-008-9115-4","volume":"42","author":"M. Bj\u00f6rk","year":"2009","unstructured":"Bj\u00f6rk, M.: First order St\u00e5lmarck. J. Autom. Reasoning\u00a042(1), 99\u2013122 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/11576280_23","volume-title":"Formal Methods and Software Engineering","author":"B. Cook","year":"2005","unstructured":"Cook, B., Gonthier, G.: Using St\u00e5lmarck\u2019s Algorithm to Prove Inequalities. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 330\u2013344. Springer, Heidelberg (2005)"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)","DOI":"10.1145\/567752.567778"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-642-33125-1_22","volume-title":"SAS 2012","author":"V. D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Satisfiability Solvers Are Static Analyzers. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 317\u2013333. Springer, Heidelberg (2012)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric Bounds Analysis with Conflict-Driven Learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"23_CR7","unstructured":"E\u00e9n, N., Sj\u00f8rensson, N.: The MiniSat solver (2006), minisat.se\/MiniSat.html"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-56287-7_95","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P. Granger","year":"1992","unstructured":"Granger, P.: Improving the Results of Static Analyses Programs by Local Decreasing Iteration (Extended Abstract). In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol.\u00a0652, pp. 68\u201379. Springer, Heidelberg (1992)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BFb0105407","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: St\u00e5lmarck\u2019s Algorithm as a HOL Derived Rule. In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 221\u2013234. Springer, Heidelberg (1996)"},{"issue":"9","key":"23_CR10","doi-asserted-by":"publisher","first-page":"1143","DOI":"10.1109\/43.310903","volume":"13","author":"W. Kunz","year":"1994","unstructured":"Kunz, W., Pradhan, D.: Recursive learning: A new implication technique for efficient solutions to CAD problems\u2013test, verification, and optimization. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a013(9), 1143\u20131158 (1994)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"23_CR11","unstructured":"Marques Silva, J., Sakallah, K.: GRASP \u2013 a new search algorithm for satisfiability. In: ICCAD (1996)"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"issue":"1","key":"23_CR13","first-page":"23","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. FMSD\u00a016(1), 23\u201358 (2000)","journal-title":"FMSD"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Spence, I.: tts: A SAT-solver for small, difficult instances. Journal on Sat., Boolean Modeling and Computation (2008), Benchmarks http:\/\/www.cs.qub.ac.uk\/~i.spence\/sdsb","DOI":"10.3233\/SAT190043"},{"key":"23_CR15","unstructured":"St\u00e5lmarck, G.: A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula (1989), Swedish Patent No. 467,076 (approved 1992); U.S. Patent No. 5,276,897 (approved 1994); European Patent No. 403,454 (approved 1995)"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"St\u00e5lmarck, G., S\u00e4flund, M.: Modeling and verifying systems and software in propositional logic. In: Int. Conf. on Safety of Computer Controls Systems (1990)","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"23_CR17","unstructured":"Thakur, A., Reps, T.: A generalization of St\u00e5lmarck\u2019s method. TR 1699 (revised), CS Dept., Univ. of Wisconsin, Madison, WI (June 2012), www.cs.wisc.edu\/wpis\/papers\/tr1699r.pdf"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A Method for Symbolic Computation of Abstract Operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 174\u2013192. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:56:14Z","timestamp":1620114974000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33125-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}