We prove an exponential lower bound on the size of proofs
in the proof system operating with ordered binary decision diagrams
introduced by Atserias, Kolaitis and Vardi. In fact, the lower bound
applies to semantic derivations operating with sets defined by OBDDs.
We do not assume ... more >>>