Abstract. We show that oblivious on-line simulation with only
polylogarithmic increase in the time and space requirements is possible
on a probabilistic (coin flipping) RAM without using any cryptographic
assumptions. The simulation will fail with a negligible probability.
If $n$ memory locations are used, then the probability of failure is ... more >>>

We study internal compression of communication protocols
to their internal entropy, which is the entropy of the transcript from the players' perspective.
We first show that errorless compression to the internal entropy
(and hence to the internal information) is impossible.
We then provide two internal compression schemes with error.
One ... more >>>

We show that the QRAT simulation algorithm of $\forall$Exp+Res from [B. Kiesl and M. Seidl, 2019] cannot be lifted to IR-calc.

more >>>

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The ... more >>>

Aaronson and Ambainis (STOC 2015, SICOMP 2018) claimed that the acceptance probability of every quantum algorithm that makes $q$ queries to an $N$-bit string can be estimated to within $\epsilon$ by a randomized classical algorithm of query complexity $O_q((N/\epsilon^2)^{1-1/2q})$. We describe a flaw in their argument but prove that the ... more >>>

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021]) is a recently introduced proof system for false QBFs. Unlike other known QBF proof systems, it builds winning strategies for the universal player within the proofs. Every line of this proof system consists of existential clauses along with countermodels. MRes stores ... more >>>

QBF proof systems are routinely adapted from propositional logic along with adjustments for the new quantifications. Existing are two main successful frameworks, the reduction and expansion frameworks, inspired by QCDCL [Zhang et al. ICCAD.'2002] and CEGAR solving [Janota et al. Artif. Intell.'2016] respectively. However, the reduction framework, while immensely useful ... more >>>