Show simple item record

dc.contributor.advisorStirling, Colin
dc.contributor.advisorBradfield, Julian
dc.contributor.authorJungteerapanich, Natthapong
dc.date.accessioned2010-11-09T10:42:11Z
dc.date.available2010-11-09T10:42:11Z
dc.date.issued2010
dc.identifier.urihttp://hdl.handle.net/1842/4208
dc.description.abstractThe main content of this thesis concerns a tableau method for solving the satisfiability problem for the modal μ-calculus. A sound and complete tableau system for the modal μ-calculus is given. Since every tableau in such tableau system is finite and bounded by the length of the formula, the tableau system may be used as a decision procedure for determining the satisfiability of the formula. An alternative proof of the small model property is obtained: every satisfiable formula has a model of size singleexponential in the length of the formula. Contrary to known proofs in literature, the results presented here do not rely on automata theory. Two simplifications of the tableau system are given. One is for the class of aconjunctive formulae. The resulting tableau system has been used to prove the completeness of Kozen’s axiomatisation with respect to the aconjunctive fragment of the modal μ- calculus. Another is for the formulae in the class Πμ 2 . In addition to the tableau method, the thesis explores some model-surgery techniques with the aim that such techniques may be used to directly prove the small model theorem. The techniques obtained so far have been used to show the small model property for Πμ 2 -formulae and for formulae with linear models.en
dc.contributor.sponsorOverseas Research Students Awards Scheme (ORSAS)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.subjecttableauxen
dc.subjectmodal logicen
dc.subjectlogicen
dc.titleTableau systems for the modal μ-calculusen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record