A Tableau Proof System with Names for Modal Mu-calculus
Colin Stirling · EPiC series in computing · 2018
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.