Formalization of modal logic S5 in the Coq proof assistant

Budaj, Lubor (2022) Formalization of modal logic S5 in the Coq proof assistant. Bachelor's Thesis, Computing Science.

Preview	Text BSc_Thesis_final.pdf Download (463kB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (132kB)

Abstract

In this thesis, we present our formalization of modal logic S5 in Coq. Firstly, we define a formula and a model as a Kripke frame. S5 is a modal logic that has an equivalence assumption on the accessibility relation in the model. Then we define an interpretation of a model with respect to Kripke semantics and a proof system. As the basis of our proof system, we use a Hilbert system. Secondly, we show the proofs of soundness and completeness. The soundness property shows that proving theorems in our proof system makes sense - we can infer only valid theorems. Completeness means that everything that is true is provable. Together, these two properties show that our proof system is suitable for proving theorems of S5. We proved the completeness of S5 using a canonical model proof. In order to do that we first had to define concepts of a consistent set of formulas and a maximal consistent set. Then we showed that formula is a countable type, allowing us to define a maximal consistent completion of a set and the canonical model. Other modal logics that have weaker assumptions about the properties of their accessibility relation, such as K, T, or S4, can be formalized in a similar way.

Item Type:	Thesis (Bachelor's Thesis)
Supervisor name:	Ramanayake, D.R.S. and Frumin, D.
Degree programme:	Computing Science
Thesis type:	Bachelor's Thesis
Language:	English
Date Deposited:	26 Aug 2022 14:19
Last Modified:	26 Aug 2022 14:19
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/28482

Actions (login required)

View Item