Daniel Leivant (Indiana University & LORIA Nancy)

Dynamic logic and its parents

Résumé: Dynamic logic for imperative programs, and similar deductive formalisms, can be seen as syntactic sugar for more explicit forms of reasoning, such as first order theories and second order logic. This view suggests notions of completeness for dynamic logic, which we argue are more informative and appropriate than the traditional notion of relative completeness.