Benedikt, Michael and Bourhis, Pierre and Boom, Michael Vanden - Definability and Interpolation within Decidable Fixpoint Logics

lmcs:4729 - Logical Methods in Computer Science, September 10, 2019, Volume 15, Issue 3
Definability and Interpolation within Decidable Fixpoint Logics

Authors: Benedikt, Michael and Bourhis, Pierre and Boom, Michael Vanden

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.


Source : oai:arXiv.org:1705.01823
Volume: Volume 15, Issue 3
Published on: September 10, 2019
Submitted on: August 1, 2018
Keywords: Computer Science - Logic in Computer Science


Share