We continue a study initiated by Krajicek of
a Resolution-like proof system working with clauses of linear
inequalities, R(CP). For all proof systems of this kind
Krajicek proved an exponential lower bound that depends
on the maximal absolute value of coefficients in the given proof and
the maximal clause width.

... more >>>

We demonstrate a family of propositional formulas in conjunctive normal form
so that a formula of size $N$ requires size $2^{\Omega(\sqrt[7]{N/logN})}$
to refute using the tree-like OBDD refutation system of
Atserias, Kolaitis and Vardi
with respect to all variable orderings.
All known symbolic quantifier elimination algorithms for satisfiability
generate ... more >>>

It is well-known that every first-order property on words is expressible
using at most three variables. The subclass of properties expressible with
only two variables is also quite interesting and well-studied. We prove
precise structure theorems that characterize the exact expressive power of
first-order logic with two variables on words. ... more >>>