Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Equivalence in QCSP (QBF)

Abstract :

The QBF validity problem with any propositional formulamay be seen as a QCSP. In this frame, we introduce a new constraint: the equivalence constraint and prove that it is stronger than equality constraint. In order to design this equivalence constraint, we introduce a new sequent calculus for QBF which is based on an equivalence relation over subformulae. This sequent calculus is proven to be sound and complete w.r.t. the semantics of the QBF. Based on this system, we define our equivalence constraint in such a way that QCSP(QBF) may be seen as a CSP(QBF) with a quantied search algorithm. We report some experiments in a generic constraint development environment.

Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-03255394
Contributeur : Okina Université d'Angers <>
Soumis le : mercredi 9 juin 2021 - 15:04:31
Dernière modification le : jeudi 10 juin 2021 - 03:39:57

Identifiants

  • HAL Id : hal-03255394, version 1
  • OKINA : ua4432

Collections

Citation

Vincent Barichard, Igor Stéphan. Equivalence in QCSP (QBF). ERCIM Workshop on Constraint Solving and Constraint Logic Programming, CSCLP'11, 2011, York, United Kingdom. pp.44 - 58. ⟨hal-03255394⟩

Partager

Métriques

Consultations de la notice

8