ridm@nrct.go.th   ระบบคลังข้อมูลงานวิจัยไทย   รายการโปรดที่คุณเลือกไว้

Tableau systems for the modal μ-calculus

หน่วยงาน Edinburgh Research Archive, United Kingdom

รายละเอียด

ชื่อเรื่อง : Tableau systems for the modal μ-calculus
นักวิจัย : Jungteerapanich, Natthapong
คำค้น : tableaux , modal logic , logic
หน่วยงาน : Edinburgh Research Archive, United Kingdom
ผู้ร่วมงาน : Stirling, Colin , Bradfield, Julian , Overseas Research Students Awards Scheme (ORSAS)
ปีพิมพ์ : 2553
อ้างอิง : http://hdl.handle.net/1842/4208
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : -
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

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

บรรณานุกรม :
Jungteerapanich, Natthapong . (2553). Tableau systems for the modal μ-calculus.
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Jungteerapanich, Natthapong . 2553. "Tableau systems for the modal μ-calculus".
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Jungteerapanich, Natthapong . "Tableau systems for the modal μ-calculus."
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2553. Print.
Jungteerapanich, Natthapong . Tableau systems for the modal μ-calculus. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2553.