3 citations · 6 across the 5 of their papers we have counts for
3 papers · 1 filter
Lifting QBF Resolution Calculi to DQBF
Olaf Beyersdorff, Leroy Chew, Renate Schmidt +1
We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (…
Selecting the Selection
Giles Reger, Martin Suda, Andrei Voronkov +1
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implement…
Finding Finite Models in Multi-Sorted First Order Logic
Giles Reger, Martin Suda, Andrei Voronkov
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and en…