Incremental determinization for quantifier elimination and functional synthesis

<a class="pub-badge pub-badge--doi" href="https://doi.org/10.1007/978-3-030-25543-5_6" rel="nofollow">DOI 10.1007/978-3-030-25543-5_6</a><a class="pub-badge pub-badge--grey" href="https://openalex.org/works/W2947778039" rel="nofollow">OpenAlex</a><a class="pub-badge pub-badge--mardi" href="https://portal.mardi4nfdi.de/wiki/Item:Q6154873" rel="nofollow">MaRDI QID Q6154873</a><a class="pub-badge pub-badge--grey" href="https://fdo.portal.mardi4nfdi.de/fdo/Q6154873" rel="nofollow">FDO</a>

Authors Markus Rabe

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Quantifier elimination, model completeness, and related topics (03C10)

Recommendations

• Quantifier Elimination via Functional Composition
• Understanding and extending incremental determinization for 2QBF
• Verification and synthesis using real quantifier elimination
• Incremental determinization
• Syntax-guided quantifier instantiation

Cited in

(2)

• Boolean functional synthesis: from under the hood of solvers
• Partial quantifier elimination and property generation

This page was built for publication: Incremental determinization for quantifier elimination and functional synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154873)