Towards the Automatic Verification of QCSP tractability results (Trabajo en progreso)

Resumen:

We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a first-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results.

Palabras Clave:

Automatic verification - Dafny - inductive predicate - proof system - tractability results

Autor(es):

• Alex Abuin {aabuin@ikerlan.es}
  Ik4-Ikerlan Research Center
  
• Hubie Chen {hubie.chen@ehu.eus }
  Universidad del País Vasco and IKERBASQUE Basque Foundation for Science
  
• Montserrat Hermo {montserrat.hermo@ehu.eus}
  Universidad del País Vasco
  
• Paqui Lucio {paqui.lucio@ehu.es}
  Universidad del País Vasco
  

Handle:

Descargas:

Este artículo tiene una licencia de uso CreativeCommons Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex