Partial quantifier elimination and property generation

DOI10.1007/978-3-031-37703-7_6MaRDI QIDQ6535530zbMATH OpenFDO

Authors Eugene Goldberg

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37703-7_6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Quantifier elimination, model completeness, and related topics (03C10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Software for quantifier elimination in propositional logic
• Fast DQBF Refutation
• New approaches to Boolean quantifier elimination
• A satisfiability procedure for quantified Boolean formulae
• Verification of partial designs using incremental QBF

Cites work

• scientific article; zbMATH DE number 1852165 (Why is no real title available?)
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• Graph-Based Algorithms for Boolean Function Manipulation
• Incremental determinization for quantifier elimination and functional synthesis
• Interpolation and SAT-based model checking.
• New methods for 3-SAT decision and worst-case analysis
• Quantifier Elimination via Functional Composition
• Quantifier elimination by dependency sequents
• SAT-Based Model Checking without Unrolling
• Software for quantifier elimination in propositional logic
• Synthesis of circular compositional program proofs via abduction
• Theory and Applications of Satisfiability Testing
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

This page was built for publication: Partial quantifier elimination and property generation

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