All reports by Author Leroy Chew:

__
TR18-102
| 15th May 2018
__

Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan#### Short Proofs in QBF Expansion

__
TR17-037
| 25th February 2017
__

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla#### Understanding Cutting Planes for QBFs

__
TR16-048
| 11th March 2016
__

Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda#### Lifting QBF Resolution Calculi to DQBF

__
TR16-005
| 22nd January 2016
__

Olaf Beyersdorff, Leroy Chew, Mikolas Janota#### Extension Variables in QBF Resolution

__
TR15-152
| 16th September 2015
__

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla#### Are Short Proofs Narrow? QBF Resolution is not Simple.

__
TR15-133
| 12th August 2015
__

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew#### Lower bounds: from circuits to QBF proof systems

__
TR15-059
| 10th April 2015
__

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla#### Feasible Interpolation for QBF Resolution Calculi

__
TR14-131
| 7th October 2014
__

Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah#### A game characterisation of tree-like Q-Resolution size

__
TR14-120
| 16th September 2014
__

Olaf Beyersdorff, Leroy Chew, Mikolas Janota#### Proof Complexity of Resolution-based QBF Calculi

__
TR14-036
| 8th March 2014
__

Mikolas Janota, Leroy Chew, Olaf Beyersdorff#### On Unification of QBF Resolution-Based Calculi

Revisions: 1

__
TR14-032
| 8th March 2014
__

Olaf Beyersdorff, Leroy Chew#### Tableau vs. Sequent Calculi for Minimal Entailment

__
TR14-014
| 28th January 2014
__

Olaf Beyersdorff, Leroy Chew#### The Complexity of Theorem Proving in Circumscription and Minimal Entailment

Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan

For quantified Boolean formulas (QBF) there are two main different approaches to solving: QCDCL and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than CDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

We define a cutting planes system CP+$\forall$red for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while ... more >>>

Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

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 (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the ... more >>>

Olaf Beyersdorff, Leroy Chew, Mikolas Janota

We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Jussila et al. '07 who ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

The groundbreaking paper `Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in ... more >>>

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF ... more >>>

Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah

We provide a characterisation for the size of proofs in tree-like Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF ... more >>>

Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important

QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular

lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique ...
more >>>

Mikolas Janota, Leroy Chew, Olaf Beyersdorff

Several calculi for quantified Boolean formulas (QBFs) exist, but

relations between them are not yet fully understood.

This paper defines a novel calculus, which is resolution-based and

enables unification of the principal existing resolution-based QBF

calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based

calculus ...
more >>>

Olaf Beyersdorff, Leroy Chew

In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (J. Autom. Reasoning, 1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e., MLK p-simulates OTAB. The simulation is technically very involved ... more >>>

Olaf Beyersdorff, Leroy Chew

Circumscription is one of the main formalisms for non-monotonic reasoning. It uses reasoning with minimal models, the key idea being that minimal models have as few exceptions as possible. In this contribution we provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate ... more >>>