{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:27:39Z","timestamp":1750307259507,"version":"3.41.0"},"reference-count":4,"publisher":"Association for Computing Machinery (ACM)","issue":"1\/2","license":[{"start":{"date-parts":[[2011,7,25]],"date-time":"2011-07-25T00:00:00Z","timestamp":1311552000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Commun. Comput. Algebra"],"published-print":{"date-parts":[[2011,7,25]]},"abstract":"<jats:p>We present four different approaches for existential Boolean quantifier elimination, based on model enumeration, resolution, knowledge compilation with projection, and substitution. We point out possible applications in the area of verification and we present preliminary benchmark results of the different approaches.<\/jats:p>","DOI":"10.1145\/2016567.2016595","type":"journal-article","created":{"date-parts":[[2011,8,10]],"date-time":"2011-08-10T16:16:22Z","timestamp":1312992982000},"page":"139-140","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["New approaches to boolean quantifier elimination"],"prefix":"10.1145","volume":"45","author":[{"given":"Christoph","family":"Zengler","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"given":"Andreas","family":"K\u00fcbler","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2011,7,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01929-6_7"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/502090.502091"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of CASC 2003","author":"Seidl A.M.","year":"2003","unstructured":"Seidl , A.M. , Sturm , T. : Boolean quantification in a first-order context . In: Proceedings of CASC 2003 . Technische Universit\u00e4t M\u00fcnchen, Garching ( 2003 ) 329--345. Seidl, A.M., Sturm, T.: Boolean quantification in a first-order context. In: Proceedings of CASC 2003. Technische Universit\u00e4t M\u00fcnchen, Garching (2003) 329--345."}],"container-title":["ACM Communications in Computer Algebra"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2016567.2016595","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2016567.2016595","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:32Z","timestamp":1750243952000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2016567.2016595"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,25]]},"references-count":4,"journal-issue":{"issue":"1\/2","published-print":{"date-parts":[[2011,7,25]]}},"alternative-id":["10.1145\/2016567.2016595"],"URL":"https:\/\/doi.org\/10.1145\/2016567.2016595","relation":{},"ISSN":["1932-2240"],"issn-type":[{"type":"print","value":"1932-2240"}],"subject":[],"published":{"date-parts":[[2011,7,25]]},"assertion":[{"value":"2011-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}