Towards Uniform Certification in QBF
We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results a...
Main Authors: | Leroy Chew, Friedrich Slivovsky |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2024-02-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/10146/pdf |
Similar Items
-
Feasible Interpolation for QBF Resolution Calculi
by: Olaf Beyersdorff, et al.
Published: (2017-06-01) -
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
by: Olaf Beyersdorff, et al.
Published: (2023-04-01) -
Uniform Interpolants in EUF: Algorithms using DAG-representations
by: Silvio Ghilardi, et al.
Published: (2022-04-01) -
Borel-piecewise continuous reducibility for uniformization problems
by: Takayuki Kihara
Published: (2017-04-01) -
Products of effective topological spaces and a uniformly computable Tychonoff Theorem
by: Robert Rettinger, et al.
Published: (2013-11-01)