Modal Logic and Separation: the Surprising Difference Between Binary and Ternary Trees

Prelegent(ci)

Jędrzej Kołodziejski

Afiliacja

University of Warsaw

Język referatu

angielski

Termin

19 listopada 2025 14:15

Pokój

p. 5440

Tytuł w języku polskim

Modal Logic and Separation: the Surprising Difference Between Binary and Ternary Trees

Seminarium

Seminarium „Teoria automatów”

---

Assume logical formulae φ,φ' which are mutually exclusive in the sense that φ entails ¬φ'. A separator is a formula ψ such that φ entails ψ and ψ entails ¬φ'. We will look at separation in the context of modal logic ML interpreted over binary trees and ternary (or higher arity) trees.

Over binary trees ML has the Craig interpolation property: every mutually exclusive φ,φ' are separated by some ψ which only uses common symbols of φ,φ'. On the contrary, over ternary trees deciding existence of such a ψ for given φ,φ' is coNEXPTIME-complete.  If time permits,  we will also discuss µ-ML, the extension of ML with fixpoints. One can ask if given φ,φ' in µ-ML are separated by some ψ in ML. This problem is EXPTIME-complete over binary trees, but 2-EXPTIME-complete over ternary ones.

This is joint work with Jean Christoph Jung.

---