Search

• < Previous
• 1
• Next >

---

Definability and Interpolation within Decidable Fixpoint Logics

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&nbsp;[&hellip;]

---

Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory

Michael Benedikt ; Cécilia Pradic ; Christoph Wernhard.

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such&nbsp;[&hellip;]

---