Output details
11 - Computer Science and Informatics
University of Kent
Output title
Existential Quantification as Incremental SAT
Type
E - Conference contribution
Name of conference/published proceedings
Twenty Third International Conference on Computer Aided Verification
Volume number
6806
Issue number
-
First page of article
191
ISSN of proceedings
1611-3349
Year of publication
2011
Number of additional authors
2
Additional information
<07> This paper represents a body of work on computing quantifier elimination in an anytime fashion that was funded by a Royal Society Joint Project with RWTH Aachen. A prequel result appears in NFM’11 and a sequel in SAS’12, the latter showing how these techniques can be extended to linear inequalities, which is itself a difficult and unexpected result. This body of work is significant because previously quantifier elimination was all or nothing; our algorithms can be stopped at any time to obtain a safe approximation of the result.
Interdisciplinary
-
Cross-referral requested
-
Research group
P - Programming Languages and Systems Group
Citation count
6
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
