Beyond Q-Resolution and Prenex Form: a Proof System for Quantified Constraint Satisfaction
| Data(s) |
03/03/2016
03/03/2016
2014
|
|---|---|
| Resumo |
We consider the quanti fied 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 quanti fication, 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. |
| Identificador |
Logical Methods in Computer Science 10(4) 2014 : (2014) // Article ID 14 1860-5974 http://hdl.handle.net/10810/17494 10.2168/LMCS-10(4:14)2014 |
| Idioma(s) |
eng |
| Publicador |
Technische Universität Braunschweig, Institute of Theoretical Computer Science |
| Relação |
http://www.lmcs-online.org/ojs/viewarticle.php?id=1627 |
| Direitos |
This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany info:eu-repo/semantics/openAccess |
| Palavras-Chave | #Q-resolution #proof system #quantified constraint satisfaction #boolean-formulas #QBFS |
| Tipo |
info:eu-repo/semantics/article |
