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

lmcs:1012 - Logical Methods in Computer Science, December 23, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:14)2014
Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint SatisfactionArticle

Authors: Hubie Chen

    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.


    Volume: Volume 10, Issue 4
    Published on: December 23, 2014
    Imported on: May 23, 2014
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,Computer Science - Computational Complexity

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1433 times.
    This article's PDF has been downloaded 312 times.