A decision procedure for semantical equivalence of thin FM specifications Original Research Article

Several authors have proposed sketches as a suitable specification mechanism for specifying databases. When specifying a database, the finite models of the specification are of greatest importance, since an actual database is of course always a finite structure. In database theory however, it has recently been recognised that it is useful to allow for a restricted kind of infiniteness in the models of a data specification. The models are then so-called metafinite structures. In this paper, we consider a sketch-based specification of metafinite structures, and we develop and prove correct an algorithm to decide the semantical equivalence of the corresponding data specifications. To the best of the authors’ knowledge, this is the first algorithm for deciding semantical equivalence for a non-trivial class of specifications for metafinite structures.