{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:58:06Z","timestamp":1760061486851,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319235059"},{"type":"electronic","value":"9783319235066"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23506-6_12","type":"book-chapter","created":{"date-parts":[[2015,9,3]],"date-time":"2015-09-03T11:50:40Z","timestamp":1441281040000},"page":"172-188","source":"Crossref","is-referenced-by-count":9,"title":["Automated Reasoning Building Blocks"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,10]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Alagi, G., Weidenbach, C.: NRCL - a model building approach to the Bernays-Sch\u00f6nfinkel fragment. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNAI, vol. 9322. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_5"},{"issue":"2","key":"12_CR2","doi-asserted-by":"crossref","first-page":"101","DOI":"10.3233\/FI-2013-855","volume":"125","author":"V Aravantinos","year":"2013","unstructured":"Aravantinos, V., Echenim, M., Peltier, N.: A resolution calculus for first-order schemata. Fundamenta Informaticae 125(2), 101\u2013133 (2013)","journal-title":"Fundamenta Informaticae"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE-10. LNCS, vol. 449, pp. 427\u2013441. Springer, Heidelberg (1990)","DOI":"10.1007\/3-540-52885-7_105"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol. I, pp. 19\u201399. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1007\/11916277_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma Learning in the Model Evolution Calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 572\u2013586. Springer, Heidelberg (2006)"},{"key":"12_CR6","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds). Handbook of Satisfiability. IOS Press (2009)"},{"issue":"7","key":"12_CR7","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. Communications of the ACM 5(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: LICS 2003, pp. 55\u201364. IEEE Computer Society (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Meyer, C., Weidenbach, C.: Soft typing for ordered resolution. In: McCune, W. (ed.) CADE-14. LNAI, vol. 1249, pp. 321\u2013335, Townsville, Australia. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63104-6_32"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Freuder, E.C. (ed.) CP. LNCS, vol. 1118, pp. 46\u201360. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61551-2_65"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"12_CR12","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-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53, 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7, vol. I, pp. 371\u2013443. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. Journal of Automated Reasoning 44(4), 401\u2013424 (2010)","DOI":"10.1007\/s10817-009-9161-6"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"12_CR16","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227. IEEE Computer Society Press (1996)"},{"key":"12_CR17","unstructured":"Smullyan, R.M.: First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer (1968) (revised republication 1995 by Dover Publications)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Teucke, A., Weidenbach, C.: First-order logic theorem proving and model building via approximation and instantiation. In: Lutz, C., Ranise, S. (eds) FroCos 2015. LNAI, vol. 9322. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_6"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds) Handbook of Automated Reasoning, ch. 27, vol. 2, pp. 1965\u20132012. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23506-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T11:47:14Z","timestamp":1748605634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-23506-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319235059","9783319235066"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23506-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}