4DL: a four-valued Dynamic logic and its proof-theory

TL;DR

This paper introduces 4DL, a four-valued dynamic logic combining Belnap's four values with dynamic logic and hybrid tools, enabling reasoning in inconsistent or incomplete systems, with a sound and complete tableaux proof system.

Contribution

It develops a novel four-valued dynamic logic integrating Belnap's logic with hybrid and dynamic logic features, along with a proof-theoretic tableaux system.

Findings

The logic is sound and complete.

The tableaux proof system terminates.

It handles inconsistent and incomplete information.

Abstract

Transition systems are often used to describe the behaviour of software systems. If viewed as a graph then, at their most basic level, vertices correspond to the states of a program and each edge represents a transition between states via the (atomic) action labelled. In this setting, systems are thought to be consistent so that at each state formulas are evaluated as either True or False. On the other hand, when a structure of this sort - for example a map where states represent locations, some local properties are known and labelled transitions represent information available about different routes - is built resorting to multiple sources of information, it is common to find inconsistent or incomplete information regarding what holds at each state, both at the level of propositional variables and transitions. This paper aims at bringing together Belnap's four values, Dynamic Logic and hybrid machinery such as nominals and the satisfaction operator, so that reasoning is still possible in face of contradicting evidence. Proof-theory for this new logic is explored by means of a terminating, sound and complete tableaux system.