Quantifier elimination and its cousin functional synthesis are fundamental problems in automated reasoning that could be used in many applications of formal methods. But, effective algorithms are still elusive. In this paper, we suggest a simple modification to a QBF algorithm to adapt it for quantifier elimination and functional synthesis. We demonstrate that the approach significantly outperforms previous algorithms for functional synthesis.
CITATION STYLE
Rabe, M. N. (2019). Incremental determinization for quantifier elimination and functional synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11562 LNCS, pp. 84–94). Springer Verlag. https://doi.org/10.1007/978-3-030-25543-5_6
Mendeley helps you to discover research relevant for your work.