| Home > Publications > Reports > Informatics (CW) |
CW 260
F. Piessens
Finite satisfiability and equivalence of finitary sketches
Abstract
A translation from classical first-order logic to sketches is given. This translation does not preserve model categories, as is usually required when one studies connections between sketches and classical string-based logic. However, the translation preserves the models in some strong sense (although it does not preserve the homomorphisms between the models). In particular, it preserves satisfiability. Based on this translation, some undecidability results from classical logic can be transported to sketches. These undecidability results have practical relevance, because sketches have been proposed by a number of authors as a very convenient formalism for specifying databases.
report.pdf / mailto: F. Piessens