# Definability and Interpolation within Decidable Fixpoint Logics

## TL;DR

This paper investigates the expressibility and definability of formulas within decidable fixpoint logics, providing semantic and effective characterizations through refined analysis of tree-model properties.

## Contribution

It introduces new methods for characterizing definability and interpolation in rich decidable fixpoint logics, enhancing understanding of their expressive power.

## Key findings

- Semantic characterizations of definability established
- Effective algorithms for formula characterization developed
- Refined analysis of tree-model property applied

## Abstract

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.