# Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction

arXiv: https://arxiv.org/abs/1403.0222 · HTML: https://mlsanity.com/paper/1403.0222/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Mar 2014.

## Built on by (most cited first, 1 of 1)

- [An Expansion-Based Approach for Quantified Integer Programming](https://mlsanity.com/paper/2506.04452/) (2025)

## Abstract (arXiv)

We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.