Skip to main content

Coalgebraic Dynamic Logic: Basic Completeness Results

Helle Hvid Hansen ( Delft University of Technology )

I will present a coalgebraic generalisation of Fischer and Ladner’s Propositional Dynamic Logic (PDL) and Parikh’s Game Logic (GL). The basic observation is that programs (or games) are coalgebras for a monad T, the program constructs arise from Kleisli composition and algebraic structure on T, and the axioms of these logics correspond to certain compatibility requirements between the modalities and this structure. This setup allows us to prove two general completeness results: strong completeness without iteration, and (weak) completeness with iteration and "negation-free" pointwise operations.

 

(Joint work with Clemens Kupke.)

Share this: