A Proof System with Names for Modal Mu-calculus
Logic in Computer Science
2013-09-23 v1
Abstract
Fixpoints are an important ingredient in semantics, abstract interpretation and program logics. Their addition to a logic can add 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 as devised by Jungteerapanich.
Keywords
Cite
@article{arxiv.1309.5129,
title = {A Proof System with Names for Modal Mu-calculus},
author = {Colin Stirling},
journal= {arXiv preprint arXiv:1309.5129},
year = {2013}
}
Comments
In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557