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

lmcs:4729 - Logical Methods in Computer Science, September 10, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:29)2019
Definability and Interpolation within Decidable Fixpoint LogicsArticle

Authors: 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.


    Volume: Volume 15, Issue 3
    Published on: September 10, 2019
    Accepted on: August 10, 2019
    Submitted on: August 1, 2018
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • DBOnto: Bridging Databases and Ontologies; Funder: UK Research and Innovation; Code: EP/L012138/1
    • ED3: Enabling analytics over Diverse Distributed Datasources; Funder: UK Research and Innovation; Code: EP/N014359/1
    • Challenges for Logic, Transducers and Automata; Funder: French National Research Agency (ANR); Code: ANR-16-CE40-0007

    Consultation statistics

    This page has been seen 1237 times.
    This article's PDF has been downloaded 268 times.