Artículo:
Towards the Automatic Verification of QCSP tractability results

Fecha

2017-07-19

Editor

Sistedes

Publicado en

Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017)

Licencia

CC BY 4.0

Resumen

We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a rst-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.

Descripción

Acerca de Abuin, Alex

Palabras clave

Automatic Verification, Dafny, Inductive Predicate, Proof System, Tractability Results

Colecciones

Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX