{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,6,28]],"date-time":"2022-06-28T01:28:01Z","timestamp":1656379681508},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,8,25]],"date-time":"2010-08-25T00:00:00Z","timestamp":1282694400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s10009-010-0167-5","type":"journal-article","created":{"date-parts":[[2010,8,24]],"date-time":"2010-08-24T01:34:27Z","timestamp":1282613667000},"page":"263-272","source":"Crossref","is-referenced-by-count":7,"title":["Reducing the size of resolution proofs in linear time"],"prefix":"10.1007","volume":"13","author":[{"given":"Omer","family":"Bar-Ilan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Fuhrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shlomo","family":"Hoory","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ohad","family":"Shacham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,8,25]]},"reference":[{"key":"167_CR1","doi-asserted-by":"crossref","unstructured":"Amla, N., McMillan, K.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS\u201903. Lecture Notes in Compuer Science, vol. 2619 (2003)","DOI":"10.1007\/3-540-36577-X_2"},{"key":"167_CR2","doi-asserted-by":"crossref","unstructured":"Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: 5th International Confrence on Formal Methods in Computer-Aided Design, FMCAD 2004, pp. 260\u2013274 (2004)","DOI":"10.1007\/978-3-540-30494-4_19"},{"key":"167_CR3","doi-asserted-by":"crossref","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Chockler, H., Hu, A. (eds.) Haifa Verification Conference (HVC\u201908). Lecture Notes in Compuer Science, vol. 5394, pp. 114\u2013128 (2008)","DOI":"10.1007\/978-3-642-01702-5_14"},{"key":"167_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907). Lecture Notes in Computer Science, pp. 358\u2013372 (2007)","DOI":"10.1007\/978-3-540-71209-1_28"},{"key":"167_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in sat modulo theories. In: SAT, pp. 334\u2013339 (2007)","DOI":"10.1007\/978-3-540-72788-0_32"},{"key":"167_CR6","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: SAT, Lecture Notes in Computer Science, vol. 4121, pp. 36\u201341. Springer, Berlin (2006)","DOI":"10.1007\/11814948_5"},{"key":"167_CR7","doi-asserted-by":"crossref","unstructured":"Fuhrman, O. Hoory, S.: On extending bounded proofs to inductive proofs. In: Proceedings of 21 st International Conference on Computer Aided Verification (CAV\u201909), (2009) (to appear)","DOI":"10.1007\/978-3-642-02658-4_23"},{"key":"167_CR8","doi-asserted-by":"crossref","unstructured":"Gershman, R., Koifman, M., Strichman, O.: Deriving small unsatisfiable cores with dominators. In: Proceedings of 18th International Conference on Computer Aided Verification (CAV\u201906). Lecture Notes in Computer Science, vol. 4144, pp. 109\u2013122 (2006)","DOI":"10.1007\/11817963_13"},{"key":"167_CR9","doi-asserted-by":"crossref","unstructured":"Gershman, R., Strichman., O.: Haifasat: A new robust SAT solver. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) First International Haifa Verification Conference. Lecture Notes in Computer Science, vol. 3875, pp. 76\u201389. Springer, Berlin (2005)","DOI":"10.1007\/11678779_6"},{"issue":"3","key":"167_CR10","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10601-007-9019-7","volume":"12","author":"\u00c9. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire \u00c9., Mazure B., Piette C.: Local-search extraction of muses. Constraints 12(3), 325\u2013344 (2007)","journal-title":"Constraints"},{"key":"167_CR11","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL \u201905: Proceedings of the 32nd ACM SIGPLAN-SIGACT sysposium on Principles of programming languages, pp. 122\u2013131. ACM Press, New York (2005)","DOI":"10.1145\/1040305.1040316"},{"key":"167_CR12","doi-asserted-by":"crossref","unstructured":"Huang, J.: Mup: A minimal unsatisfiability prover. In: Proceedings of the 10th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 432\u2013437 (2005)","DOI":"10.1145\/1120725.1120907"},{"key":"167_CR13","doi-asserted-by":"crossref","unstructured":"Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D. (eds.) Proceedings of 16th International Conference on Computer Aided Verification (CAV\u201904), LNCS, vol. 3114, pp. 308\u2013320. Springer, Boston (2004)","DOI":"10.1007\/978-3-540-27813-9_24"},{"issue":"1","key":"167_CR14","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T. Lengauer","year":"1979","unstructured":"Lengauer T., Tarjan R.E.: A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst. 1(1), 121\u2013141 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"167_CR15","unstructured":"Lynce, I., Marques-Silva, J.: On computing minimum unsatisfiable cores. In: Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, pp. 305\u2013310 (2004)"},{"key":"167_CR16","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Interpolation and sat-based model checking. In: Warren, J., Hunt, A., Somenzi, F. (eds.) cav03. Lecture Notes in Computer Science (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"167_CR17","doi-asserted-by":"crossref","unstructured":"Mneimneh, M.N., Lynce, I., Andraus, Z.S., Silva, J.P.M., Sakallah, K.A.: A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In: SAT. Lecture Notes in Computer Science, vol. 3569, pp. 467\u2013474. Springer, Berlin (2005)","DOI":"10.1007\/11499107_40"},{"key":"167_CR18","doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: Amuse: a minimally-unsatisfiable subformula extractor. In: DAC \u201904, pp. 518\u2013523 (2004)","DOI":"10.1145\/996566.996710"},{"issue":"1","key":"167_CR19","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","volume":"37","author":"C.H. Papadimitriou","year":"1988","unstructured":"Papadimitriou C.H., Wolfe D.: The complexity of facets resolved. J. Comput. Syst. Sci. 37(1), 2\u201313 (1988)","journal-title":"J. Comput. Syst. Sci."},{"key":"167_CR20","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master\u2019s thesis, Simon Fraser University (2004)"},{"key":"167_CR21","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Prunning techniques for the SAT-based bounded model checking problem. In: Proceedings of the 11th Conference on Correct Hardware Design and Verification Methods (CHARME\u201901), Edinburgh (2001)","DOI":"10.1007\/3-540-44798-9_4"},{"key":"167_CR22","unstructured":"Tseitin, G.: On the complexity of proofs in poropositional logics. In: Siekmann, J., Wrightson, G. (eds.), Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, vol. 2. Springer, Berlin (1983) [Originally published (1970)]"},{"issue":"4","key":"167_CR23","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"Urquhart A.: The complexity of propositional proofs. Bull. Symbol. Logic 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symbol. Logic"},{"key":"167_CR24","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: Satire: a new incremental satisfiability engine. In: In IEEE\/ACM Design Automation Conference (DAC) (2001)","DOI":"10.1145\/378239.379019"},{"key":"167_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: ICCAD (2001)","DOI":"10.1145\/774572.774637"},{"key":"167_CR26","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), S. Margherita Ligure (2003)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0167-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0167-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0167-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T02:51:57Z","timestamp":1559443917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0167-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8,25]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["167"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0167-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8,25]]}}}