MAS: Using Priest Modal Tableaux to Visualise Kripke Models
Chapter 1: Introduction
M. Koonstra S2399385 / G. Schoenmacker s1550748 / Rijksuniversiteit Groningen
MAS
The abbreviation MAS stands for 'Multi-Agent Systems', a course given at the Rijksuniversiteit Groningen. The contents and objectives of the course can be found at the Ocasys page for the course.
One of the requirements of the course is a project, the result of which it to be presented on a website. This website contains the presentation of one of these projects.
Modal Logic and Kripke models
Modal logic is the extension of classical logic to include the concept of modality, which intuitively can be defined as the capability to reason about possible alternative realities. The semantics of this new logic (Kripke semantics) as well as the intuitive representation of same (Kripke models) are named after the creator, American philosopher and logician Saul Kripke. The possible-world semantics Kripke introduced can be represented by a graph of connected nodes, in which the nodes represent possible worlds and the edges represent connections between these worlds for agents reasoning in the model. For example, imagine a model in which the following formulae are true:
M ⊨ K1 p ∨ K1 ¬pM ⊨ K2 q ∨ K2 ¬q
This world can be represented using the following graph:
Project summary
We applied the theory from the MAS course to implement a counter-model visualisation computer application for the logic systems K and S5 using Priest modal tableaux. This means we created a computer program which can (1) automatically prove whether a formula in either of these systems is a tautology; and (2) can visualise either a model if the formula is a tautology or a counter model if the formula is no tautology. To achieve this, we implemented a semantic tableaux system introduced by J. Priest in a his book "An Introduction to Non-Classical Logic".
Our program works in propositional logic, systems K(m), KEC(m), S5(m) and S5EC(m). It can visualise all found models or counter models a formula produces.
In the following section, we shall introduce the theoretic foundations of our project. After that, we shall show how we applied these theories in our computer program. Next, we will demonstrate the resulting program as a whole, showing the fruits of our labour. Following that, we will discuss some interesting examples and present our conclusions and discuss shortcomings of the current implementation. Lastly, we list our sources.
Next Chapter: Chapter 2 - Theory
