Paul Beame

Proof complexity, the study of the lengths of proofs in

propositional logic, is an area of study that is fundamentally connected

both to major open questions of computational complexity theory and

to practical properties of automated theorem provers. In the last

decade, there have been a number of significant advances ...
more >>>

Till Tantau

Kummer's cardinality theorem states that a language is recursive

if a Turing machine can exclude for any n words one of the

n + 1 possibilities for the number of words in the language. It

is known that this theorem does not hold for polynomial-time

computations, but there ...
more >>>

Tomas Feder

Attempts at classifying computational problems as polynomial time

solvable, NP-complete, or belonging to a higher level in the polynomial

hierarchy, face the difficulty of undecidability. These classes, including

NP, admit a logic formulation. By suitably restricting the formulation, one

finds the logic class MMSNP, or monotone monadic strict NP without

more >>>

Tomas Feder, Phokion G. Kolaitis

Quantified constraint satisfaction is the generalization of

constraint satisfaction that allows for both universal and existential

quantifiers over constrained variables, instead

of just existential quantifiers.

We study quantified constraint satisfaction problems ${\rm CSP}(Q,S)$, where $Q$ denotes

a pattern of quantifier alternation ending in exists or the set of all possible

more >>>

Walid Gomaa

Model theory is a branch of mathematical logic that investigates the

logical properties of mathematical structures. It has been quite

successfully applied to computational complexity resulting in an

area of research called descriptive complexity theory. Descriptive

complexity is essentially a syntactical characterization of

complexity classes using logical formalisms. However, there ...
more >>>

Matthew Anderson, Dieter van Melkebeek, Nicole Schweikardt, Luc Segoufin

We study the locality of an extension of first-order logic that captures graph queries computable in AC$^0$, i.e., by families of polynomial-size constant-depth circuits. The extension considers first-order formulas over relational structures which may use arbitrary numerical predicates in such a way that their truth value is independent of the ... more >>>

Lakhdar Saïs, Mohand-Saïd Hacid, francois hantry

We show that (1) the Minimal False QCNF search problem (MF-search) and

the Minimal Unsatisfiable LTL formula search problem (MU-search) are FPSPACE complete because of the very expressive power of QBF/LTL, (2) we extend the PSPACE-hardness of the MF decision problem to the MU decision problem. As a consequence, we ...
more >>>