3 citations · 6 across the 2 of their papers we have counts for
5 papers
Blocked Clauses in First-Order Logic
Benjamin Kiesl, Martin Suda, Martina Seidl +2
Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees t…
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…
Duality in STRIPS planning
Martin Suda
We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its p…