Navegación

Búsqueda

Búsqueda avanzada

El autor Montserrat Hermo ha publicado 5 artículo(s):

1 - Learning a Subclass of Multivalued Dependencies Formulas from Entailments

Functional and multivalued dependencies play an important role in the design of relational databases. There is a strong connection between data dependencies and some fragments of the propositional logic. In particular, functional dependencies are closely related to Horn formulas. Also, multivalued dependencies are characterized in terms of multivalued formulas. It is known that both Horn formulas and sets of functional dependencies are efficiently learnable in the exact model of learning with queries. In this work, we study the learnability of a non-trivial subclass of multivalued formulas called CRMVDF. We use Angluin’s exact learning model with membership and equivalence queries and present a polynomial time algorithm which exactly learns CRMVDF from entailments.

Autores: Montserrat Hermo / Ana Ozaki / 
Palabras Clave:

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

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.

Autores: Alex Abuin / Hubie Chen / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Automatic verification - Dafny - inductive predicate - proof system - tractability results

3 - Context-based Model Checking using SMT-solvers (Trabajo en progreso)

In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.

Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Model checking - SAT - SMT - Solvers - Tableux

4 -