A Tableau Proof System with Names for Modal Mu-calculus

Colin Stirling

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationHOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday
Pages306-318
Number of pages13
Volume42
DOIs
Publication statusPublished - 12 Feb 2014

Fingerprint

Dive into the research topics of 'A Tableau Proof System with Names for Modal Mu-calculus'. Together they form a unique fingerprint.

Cite this