10 citations · 17 across the 11 of their papers we have counts for
8 papers · 1 filter
Proof Systems for the Modal -Calculus Obtained by Determinizing Automata
Maurice Dekker, Johannes Kloibhofer, Johannes Marti +1
Automata operating on infinite objects feature prominently in the theory of the modal -calculus. One such application concerns the tableau games introduced by Niwiński & Walukie…
On the size of disjunctive formulas in the -calculus
Clemens Kupke, Johannes Marti, Yde Venema
A key result in the theory of the modal mu-calculus is the disjunctive normal form theorem by Janin & Walukiewicz, stating that every mu-calculus formula is semantically equivalent…
Focus-style proof systems and interpolation for the alternation-free -calculus
Johannes Marti, Yde Venema
In this paper we introduce a cut-free sequent calculus for the alternation-free fragment of the modal -calculus. This system allows for cyclic proofs and uses a simple focus mec…
Size matters in the modal -calculus
Clemens Kupke, Johannes Marti, Yde Venema
We discuss and compare complexity measures for the modal -calculus, focusing on size and alternation depth. As a yardstick we take Wilke's alternating tree automata, which we sh…
Conditional Logic is Complete for Convexity in the Plane
Johannes Marti
We prove completeness of preferential conditional logic with respect to convexity over finite sets of points in the Euclidean plane. A conditional is defined to be true in a finite…
Completeness for Game Logic
Sebastian Enqvist, Helle Hvid Hansen, Clemens Kupke +2
Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-…
Parity Games and Automata for Game Logic (Extended Version)
Helle Hvid Hansen, Clemens Kupke, Johannes Marti +1
Parikh's game logic is a PDL-like fixpoint logic interpreted on monotone neighbourhood frames that represent the strategic power of players in determined two-player games. Game log…
Uniform Interpolation for Coalgebraic Fixpoint Logic
Johannes Marti, Fatemeh Seifan, Yde Venema
We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the…