Definability and Interpolation within Decidable Fixpoint LogicsArticle
Authors: Michael Benedikt ; Pierre Bourhis ; Michael Vanden Boom
NULL##NULL##NULL
Michael Benedikt;Pierre Bourhis;Michael Vanden Boom
We look at characterizing which formulas are expressible in rich decidable
logics such as guarded fixpoint logic, unary negation fixpoint logic, and
guarded negation fixpoint logic. We consider semantic characterizations of
definability, as well as effective characterizations. Our algorithms revolve
around a finer analysis of the tree-model property and a refinement of the
method of moving back and forth between relational logics and logics over
trees.