{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T08:02:23Z","timestamp":1791964943781,"version":"4.3.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642026577","type":"print"},{"value":"9783642026584","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_30","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T11:00:16Z","timestamp":1245668416000},"page":"383-397","source":"Crossref","is-referenced-by-count":21,"title":["Quantifier Elimination via Functional Composition"],"prefix":"10.1007","author":[{"given":"Jie-Hong R.","family":"Jiang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification (2005), http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"30_CR2","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Heidelberg (1998)"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Coudert, O., Madre, J.C.: A unified framework for the formal verification of sequential circuits. In: Proc. Int\u2019l. Conf. Computer-Aided Design, pp. 126\u2013129 (1990)","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"issue":"3","key":"30_CR5","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"J. Symbolic Logic"},{"key":"30_CR6","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"2000","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, London (2000)","edition":"2"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: Proc. Int\u2019l. Conf. Computer-Aided Design, pp. 510\u2013517 (2004)","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 39\u201351. Springer, Heidelberg (2005)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Lee, R.-R., Jiang, J.-H.R., Hung, W.-L.: Bi-decomposing large Boolean functions via interpolation and satisfiability solving. In: Proc. Design Automation Conf., pp. 636\u2013641 (2008)","DOI":"10.1145\/1391469.1391634"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Lee, C.-C., Jiang, J.-H.R., Huang, C.-Y., Mishchenko, A.: Scalable exploration of functional dependency by interpolation and incremental SAT solving. In: Proc. Int\u2019l. Conf. on Computer-Aided Design, pp. 227\u2013233 (2007)","DOI":"10.1109\/ICCAD.2007.4397270"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Lin, H.-P., Jiang, J.-H.R., Lee, R.-R.: To SAT or not to SAT: Ashenhurst decomposition in a large scale. In: Proc. Int\u2019l. Conf. Computer-Aided Design, pp. 32\u201337 (2008)","DOI":"10.1109\/ICCAD.2008.4681548"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Brayton, R.K., Jiang, J.-H.R., Jang, S.: Scalable don\u2019t-care-based logic optimization and resynthesis. In: Proc. Int\u2019l. Symp. on Field Programmable Gate Arrays, pp. 151\u2013160 (2009)","DOI":"10.1145\/1508128.1508152"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Proc. Design Automation Conference, pp. 532\u2013536 (2006)","DOI":"10.1145\/1146909.1147048"},{"key":"30_CR14","unstructured":"Mishchenko, A., Chatterjee, S., Jiang, J.-H.R., Brayton, R.K.: FRAIGs: A unifying representation for logic synthesis and verification. Technical Report, EECS Dept., UC Berkeley (2005)"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2002","unstructured":"McMillan, K.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2003","unstructured":"McMillan, K.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Scholl, C., Disch, S.: Advanced unbounded model checking based on AIGs, BDD sweeping, and quantifier scheduling. In: Proc. Formal Methods on Computer Aided Design, pp. 89\u201396 (2006)","DOI":"10.1109\/FMCAD.2006.4"},{"key":"30_CR18","first-page":"125","volume":"10","author":"T. Skolem","year":"1928","unstructured":"Skolem, T.: Uber die mathematische Logik. Norsk. Mat. Tidsk.\u00a010, 125\u2013142 (1928); Translation in From Frege to G\u00f6del, A Source Book in Mathematical Logic, J. van Heijenoort. Harvard Univ. Press (1967)","journal-title":"Norsk. Mat. Tidsk."},{"key":"30_CR19","unstructured":"Seidl, A., Sturm, T.: Boolean quantification in a first-order context. In: Proc. Int\u2019l. Workshop on Computer Algebra in Scientific Computing, pp. 329\u2013345 (2003)"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Sturm, T.: New domains for applied quantifier elimination. In: Proc. Int\u2019l. Workshop on Computer Algebra in Scientific Computing, pp. 295\u2013301 (2006)","DOI":"10.1007\/11870814_25"},{"key":"30_CR21","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Touati, H., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit enumeration of finite state machines using BDDs. In: Proc. Int\u2019l. Conf. on Computer-Aided Design, pp. 130\u2013133 (1990)","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"30_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation\u00a05, 3\u201327 (1988)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T07:58:22Z","timestamp":1739174302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}