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.
翻译：4DL：一种四值动态逻辑及其证明理论
Translated abstract:
本文旨在将贝尔纳普的四值、动态逻辑以及名称和满足操作等混合机制结合起来，以使在面对相互矛盾的证据时仍然可以进行推理。通过终止、完备、 sound的 tableau 系统探讨了这种新逻辑的证明理论。通常情况下，如果将转换系统视为图形，则可以将其用于描述软件系统的行为。在最基本的水平上，顶点对应于程序的状态，每个边表示通过标记的（原子）操作在状态之间的转换。在这种情况下，将系统视为一致的，以便在每个状态下将公式评估为 True 或 False。然而，当构建这种结构（例如地图）时，其中状态表示位置，已知一些局部属性，标记的转换表示有关不同路线的信息，这样多个信息源之间存在不一致或不完整的信息，无论在命题变量和转换的级别上。
相关内容
微信扫码咨询专知VIP会员