Strategy extraction by interpolation
From MaRDI portal
Cites work
- Constructing Craig interpolation formulas
- Expansion-based QBF solving versus Q-resolution
- Extended Resolution Proofs for Conjoining BDDs
- Feasible interpolation for QBF resolution calculi
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- How QBF expansion makes strategy extraction hard
- scientific article; zbMATH DE number 5899257 (Why is no real title available?)
- scientific article; zbMATH DE number 5510691 (Why is no real title available?)
- Interpolant strength
- Interpolation and SAT-based model checking.
- Interpolation and Symbol Elimination
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Introduction: Interpolations -- essays in honor of William Craig
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Local soundness for QBF calculi
- Long-distance Q-resolution with dependency schemes
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Multi-linear strategy extraction for QBF expansion proofs via local soundness
- New resolution-based QBF calculi and their proof complexity
- On exponential lower bounds for partially ordered resolution
- Polynomial-time validation of QCDCL certificates
- SAT-Based Synthesis Methods for Safety Specs
- Solving QBF with counterexample guided refinement
- Towards uniform certification in QBF
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Unified QBF certification and its applications
This page was built for publication: Strategy extraction by interpolation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6864410)
