Show simple item record

dc.contributor.authorChen, Hubert Ming
dc.date.accessioned2016-03-03T13:19:24Z
dc.date.available2016-03-03T13:19:24Z
dc.date.issued2014
dc.identifier.citationLogical Methods in Computer Science 10(4) : (2014) // Article ID 14es
dc.identifier.issn1860-5974
dc.identifier.urihttp://hdl.handle.net/10810/17494
dc.description.abstractWe 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.es
dc.description.sponsorshipThe author thanks Moritz Muller and Friedrich Slivovsky for useful comments. This work was supported by the Spanish project TIN2013-46181-C2-2-R, by the Basque project GIU12/26, and by the Basque grant UFI11/45.es
dc.language.isoenges
dc.publisherTechnische Universität Braunschweig, Institute of Theoretical Computer Sciencees
dc.rightsinfo:eu-repo/semantics/openAccesses
dc.subjectQ-resolutiones
dc.subjectproof systemes
dc.subjectquantified constraint satisfactiones
dc.subjectboolean-formulases
dc.subjectQBFSes
dc.titleBeyond Q-Resolution and Prenex Form: a Proof System for Quantified Constraint Satisfactiones
dc.typeinfo:eu-repo/semantics/articlees
dc.rights.holderThis 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, Germanyes
dc.relation.publisherversionhttp://www.lmcs-online.org/ojs/viewarticle.php?id=1627es
dc.identifier.doi10.2168/LMCS-10(4:14)2014
dc.departamentoesLenguajes y sistemas informáticoses_ES
dc.departamentoeuHizkuntza eta sistema informatikoakes_ES
dc.subject.categoriaCOMPUTER SCIENCE, MULTIDISCIPLINARY
dc.subject.categoriaTHEORETICAL COMPUTER SCIENCE


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record