Howard Barringer was a pioneer in the study of temporal logics with fixpoints. Their addition adds considerable expressive power. One general issue is how to define proof systems for such logics. Here we examine proof systems for modal logic with fixpoints. We present a tableau proof system for checking validity of formulas which uses names to keep track of unfoldings of fixpoint variables.
|Title of host publication||HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday|
|Number of pages||13|
|Publication status||Published - 12 Feb 2014|