| Publication | Date of Publication | Type |
|---|
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
Formal Methods in System Design | 2021-12-08 | Paper |
QRATPre+: effective QBF preprocessing via strong redundancy properties
(available as arXiv preprint) | 2020-05-20 | Paper |
\textsf{Ko\(_{\mathsf{M}}\)eT}
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
On the practical value of different definitional translations to normal form
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
Non-elementary speed-ups in proof length by different variants of classical analytic calculi
Lecture Notes in Computer Science | 2019-01-15 | Paper |
Lean induction principles for tableaux
Lecture Notes in Computer Science | 2019-01-15 | Paper |
\({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
(available as arXiv preprint) | 2018-10-18 | Paper |
DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
(available as arXiv preprint) | 2017-09-22 | Paper |
Conformant planning as a case study of incremental QBF solving
Annals of Mathematics and Artificial Intelligence | 2017-08-15 | Paper |
On Stronger Calculi for QBFs
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Q-resolution with generalized axioms
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Automated benchmarking of incremental SAT and QBF solvers
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Enhancing search-based QBF solving by dynamic blocked clause elimination
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Complexity Classifications for Logic-Based Argumentation
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Exact location of the phase transition for random \((1,2)\)-QSAT
RAIRO - Theoretical Informatics and Applications | 2015-04-15 | Paper |
Incremental QBF solving by DepQBF
Mathematical Software – ICMS 2014 | 2014-09-08 | Paper |
Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
On sequent systems and resolution for QBFs
Theory and Applications of Satisfiability Testing – SAT 2012 | 2013-08-12 | Paper |
Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
Theory and Applications of Satisfiability Testing – SAT 2013 | 2013-08-05 | Paper |
| Answer-set programming encodings for argumentation frameworks | 2011-11-23 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2009-07-24 | Paper |
A solver for QBFs in negation normal form
Constraints | 2009-05-29 | Paper |
scientific article; zbMATH DE number 5547881 (Why is no real title available?)
(available as arXiv preprint) | 2009-04-28 | Paper |
Proof-complexity results for nonmonotonic reasoning
ACM Transactions on Computational Logic | 2008-12-21 | Paper |
New Results on the Phase Transition for Random Quantified Boolean Formulas
Theory and Applications of Satisfiability Testing – SAT 2008 | 2008-05-27 | Paper |
On deciding subsumption problems
Annals of Mathematics and Artificial Intelligence | 2005-05-13 | Paper |
| scientific article; zbMATH DE number 2090289 (Why is no real title available?) | 2004-08-12 | Paper |
On different proof-search strategies for orthologic
Studia Logica | 2003-04-27 | Paper |
Practically useful variants of definitional translations to normal form
Information and Computation | 2003-01-14 | Paper |
| scientific article; zbMATH DE number 1748576 (Why is no real title available?) | 2002-11-13 | Paper |
| Normal form transformations | 2002-08-27 | Paper |
| scientific article; zbMATH DE number 1765700 (Why is no real title available?) | 2002-07-10 | Paper |
On different intuitionistic calculi and embeddings from Int to S4
Studia Logica | 2002-06-13 | Paper |
| scientific article; zbMATH DE number 1552525 (Why is no real title available?) | 2001-07-29 | Paper |
| scientific article; zbMATH DE number 1552519 (Why is no real title available?) | 2001-07-03 | Paper |
| scientific article; zbMATH DE number 1612552 (Why is no real title available?) | 2001-07-01 | Paper |
| scientific article; zbMATH DE number 1389648 (Why is no real title available?) | 2000-01-17 | Paper |
| scientific article; zbMATH DE number 1342207 (Why is no real title available?) | 1999-09-22 | Paper |
| scientific article; zbMATH DE number 1324437 (Why is no real title available?) | 1999-08-16 | Paper |
| scientific article; zbMATH DE number 1231696 (Why is no real title available?) | 1999-01-10 | Paper |
| scientific article; zbMATH DE number 1189101 (Why is no real title available?) | 1999-01-05 | Paper |
| scientific article; zbMATH DE number 1222428 (Why is no real title available?) | 1998-11-11 | Paper |
An answer to an open problem of Urquhart
Theoretical Computer Science | 1998-08-13 | Paper |
| scientific article; zbMATH DE number 1088197 (Why is no real title available?) | 1997-11-17 | Paper |
| scientific article; zbMATH DE number 994053 (Why is no real title available?) | 1997-09-29 | Paper |
On different structure-preserving translations to normal form
Journal of Symbolic Computation | 1997-03-06 | Paper |
| scientific article; zbMATH DE number 516991 (Why is no real title available?) | 1994-03-17 | Paper |
| scientific article; zbMATH DE number 517073 (Why is no real title available?) | 1994-03-17 | Paper |
