A Proof System with Names for Modal Mu-calculus

A Proof System with Names for Modal Mu-calculus

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...

Full description

Bibliographic Details
Main Author: Colin Stirling
Format: Article
Language:English
Published: Open Publishing Association 2013-09-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1309.5129v1
id doaj-db116bad5cf4425e8266c8ca4d57f28a
record_format Article
spelling doaj-db116bad5cf4425e8266c8ca4d57f28a2020-11-24T21:05:31ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-09-01129Festschrift for Dave Schmidt182910.4204/EPTCS.129.2A Proof System with Names for Modal Mu-calculusColin StirlingFixpoints 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. http://arxiv.org/pdf/1309.5129v1
collection DOAJ
language English
format Article
sources DOAJ
author Colin Stirling
spellingShingle Colin Stirling
A Proof System with Names for Modal Mu-calculus
Electronic Proceedings in Theoretical Computer Science
author_facet Colin Stirling
author_sort Colin Stirling
title A Proof System with Names for Modal Mu-calculus
title_short A Proof System with Names for Modal Mu-calculus
title_full A Proof System with Names for Modal Mu-calculus
title_fullStr A Proof System with Names for Modal Mu-calculus
title_full_unstemmed A Proof System with Names for Modal Mu-calculus
title_sort proof system with names for modal mu-calculus
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2013-09-01
description 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.
url http://arxiv.org/pdf/1309.5129v1
work_keys_str_mv AT colinstirling aproofsystemwithnamesformodalmucalculus
AT colinstirling proofsystemwithnamesformodalmucalculus
_version_ 1716768470570369024

Similar Items