Does QRAT simulate IR-calc? QRAT simulation algorithm for $\forall$Exp+Res cannot be lifted to IR-calc

TL;DR

This paper demonstrates that the QRAT simulation algorithm for the $orall$Exp+Res proof system cannot be extended or adapted to work with the IR-calc proof system, highlighting fundamental limitations.

Contribution

It provides a formal proof that the QRAT simulation algorithm cannot be generalized to IR-calc, clarifying the boundaries of proof system simulations.

Findings

QRAT simulation algorithm cannot be lifted to IR-calc

Highlights limitations in proof system simulations

Clarifies boundaries between proof systems

Abstract

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