{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T23:56:49Z","timestamp":1794527809732,"version":"4.9.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319449524","type":"print"},{"value":"9783319449531","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-44953-1_54","type":"book-chapter","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T11:12:23Z","timestamp":1471864343000},"page":"859-875","source":"Crossref","is-referenced-by-count":0,"title":["Finding Unsatisfiable Cores of a Set of Polynomials Using the Gr\u00f6bner Basis Algorithm"],"prefix":"10.1007","author":[{"given":"Xiaojun","family":"Sun","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Irina","family":"Ilioaea","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Priyank","family":"Kalla","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Enescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,8,23]]},"reference":[{"key":"54_CR1","unstructured":"de Siqueira, J.L., Puget, J.-F.: Explanation-based generalization of failures. In: Proceedings of European Conference Artificial Intelligence, pp. 339\u2013344 (1988)"},{"issue":"4","key":"54_CR2","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1109\/TC.2010.12","volume":"59","author":"J-HR Jiang","year":"2010","unstructured":"Jiang, J.-H.R., Lee, C.-C., Mishchenko, A., Huang, C.-Y.: To SAT or Not to SAT: scalable exploration of functional dependency. IEEE Trans. Comp. 59(4), 457\u2013466 (2010)","journal-title":"IEEE Trans. Comp."},{"issue":"5","key":"54_CR3","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"54_CR4","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: models, algorithms and applications. In: IEEE International Symposium on Multi-Valued Logic, pp. 9\u201314 (2010)","DOI":"10.1109\/ISMVL.2010.11"},{"key":"54_CR5","doi-asserted-by":"crossref","first-page":"27","DOI":"10.3233\/SAT190100","volume":"9","author":"A Nadel","year":"2014","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Accelerated deletion-based extraction of minimal unsatisfiable cores. J. Satisfiability Boolean Model. Comput. 9, 27\u201351 (2014)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"issue":"2","key":"54_CR6","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"54_CR7","doi-asserted-by":"crossref","DOI":"10.1090\/gsm\/003","volume-title":"An Introduction to Gr\u00f6bner Bases","author":"WW Adams","year":"1994","unstructured":"Adams, W.W., Loustaunau, P.: An Introduction to Gr\u00f6bner Bases. American Mathematical Society, Providence (1994)"},{"key":"54_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-35651-8","volume-title":"Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"D Cox","year":"2007","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, New York (2007)"},{"key":"54_CR9","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Rest-klassen-ringes nach einem nulldimensionalen Polynomideal, Ph.D. Dissertation. Philosophiesche Fakultat an der Leopold-Franzens-Universitat, Austria (1965)"},{"key":"54_CR10","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Gr\u00f6bner basis algorithm to find proofs of unsatisfiability. In: ACM Symposium on Theory of Computing, pp. 174\u2013183 (1996)","DOI":"10.1145\/237814.237860"},{"key":"54_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1112\/plms\/s3-73.1.1","volume":"73","author":"P Beame","year":"1996","unstructured":"Beame, P., Impagliazzo, R., Kraji\u010dek, J., Pitassi, T., Pudl\u00e1k, P.: Lower bounds on Hilbert\u2019s Nullstellensatz and propositional proofs. Proc. Lond. Math. Soc. 73, 1\u201326 (1996)","journal-title":"Proc. Lond. Math. Soc."},{"key":"54_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1007\/978-3-540-71209-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Condrat","year":"2007","unstructured":"Condrat, C., Kalla, P.: A Gr\u00f6bner basis approach to CNF-formulae preprocessing. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 618\u2013631. Springer, Heidelberg (2007)"},{"key":"54_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-642-15274-0_26","volume-title":"Computer Algebra in Scientific Computing","author":"C Zengler","year":"2010","unstructured":"Zengler, C., K\u00fcchlin, W.: Extending clause learning of SAT solvers with Boolean Gr\u00f6bner bases. In: Gerdt, V.P., Koepf, W., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2010. LNCS, vol. 6244, pp. 293\u2013302. Springer, Heidelberg (2010)"},{"issue":"9","key":"54_CR14","doi-asserted-by":"crossref","first-page":"1326","DOI":"10.1016\/j.jsc.2008.02.017","volume":"44","author":"M Brickenstein","year":"2009","unstructured":"Brickenstein, M., Dreyer, A.: Polybori: a framework for Gr\u00f6bner basis computations with Boolean polynomials. J. Symbolic Comput. 44(9), 1326\u20131345 (2009)","journal-title":"J. Symbolic Comput."},{"key":"54_CR15","unstructured":"Vardi, M.Y., Tran, Q.: Groebner bases computation in Boolean rings for symbolic model checking. In: IASTED (2007)"},{"issue":"3","key":"54_CR16","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0377-2217(81)90177-6","volume":"8","author":"JNM Loon van","year":"1981","unstructured":"van Loon, J.N.M.: Irreducibly inconsistent systems of linear inequalities. Eur. J. Oper. Res. 8(3), 283\u2013288 (1981)","journal-title":"Eur. J. Oper. Res."},{"issue":"2","key":"54_CR17","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"JW Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3(2), 157\u2013168 (1991)","journal-title":"INFORMS J. Comput."},{"key":"54_CR18","unstructured":"Decker, W., Greuel, G.-M., Pfister, G., Sch\u00f6nemann, H.: Singular 3\u20131-3 \u2014 A computer algebra system for polynomial computations (2011). http:\/\/www.singular.uni-kl.de"},{"issue":"2","key":"54_CR19","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/BF00196789","volume":"3","author":"GB Agnew","year":"1991","unstructured":"Agnew, G.B., Mullin, R.C., Onyszchuk, I., Vanstone, S.A.: An implementation for a fast public-key cryptosystem. J. Cryptology 3(2), 63\u201379 (1991)","journal-title":"J. Cryptology"},{"issue":"2","key":"54_CR20","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1109\/TC.2005.29","volume":"54","author":"A Reyhani-Masoleh","year":"2005","unstructured":"Reyhani-Masoleh, A., Hasan, M.A.: Low complexity word-level sequential normal basis multipliers. IEEE Trans. Comput. 54(2), 98\u2013110 (2005)","journal-title":"IEEE Trans. Comput."},{"issue":"9","key":"54_CR21","doi-asserted-by":"crossref","first-page":"1409","DOI":"10.1109\/TCAD.2013.2259540","volume":"32","author":"J Lv","year":"2013","unstructured":"Lv, J., Kalla, P., Enescu, F.: Efficient Gr\u00f6bner basis reductions for formal verification of Galois field arithmetic circuits. IEEE Trans. CAD 32(9), 1409\u20131420 (2013)","journal-title":"IEEE Trans. CAD"},{"key":"54_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-21493-6_9","volume-title":"Algebraic Informatics","author":"S Gao","year":"2011","unstructured":"Gao, S., Platzer, A., Clarke, E.M.: Quantifier elimination over finite fields using Gr\u00f6bner bases. In: Winkler, F. (ed.) CAI 2011. LNCS, vol. 6742, pp. 140\u2013157. Springer, Heidelberg (2011)"},{"key":"54_CR23","unstructured":"Kalla, P.: Formal verification of arithmetic datapaths using algebraic geometry and symbolic computation. In: Invited Tutorial, Proceedings of FMCAD, p. 2 (2015). http:\/\/www.cs.utexas.edu\/users\/hunt\/FMCAD\/FMCAD15\/slides\/fmcad15-tutorial-kalla.pdf"},{"key":"54_CR24","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed, A., Gro\u00dfe, D., K\u00fchne, U., Soeken, M., Drechsler, R.: Formal verification of integer multipliers by combining Gr\u00f6bner basis with logic reduction. In: Proceedings of Design Automation and Test in Europe, pp. 1048\u20131053 (2016)","DOI":"10.3850\/9783981537079_0248"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44953-1_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,25]],"date-time":"2020-09-25T07:59:59Z","timestamp":1601020799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44953-1_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319449524","9783319449531"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44953-1_54","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-44953-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}