论文标题
4DL：四值动态逻辑及其证明理论
4DL: a four-valued Dynamic logic and its proof-theory
论文作者
论文摘要
过渡系统通常用于描述软件系统的行为。如果将其视为图形，则在其最基本的层面上，顶点对应于程序的状态，每个边缘代表通过标记的（原子）操作之间的状态之间的过渡。在这种情况下，系统被认为是一致的，因此在每个状态公式下被评估为True或false。 另一方面，当此类结构（例如状态代表位置的地图）时，某些局部属性是已知和标记的过渡表示有关不同路线的可用信息 - 构建了诉诸多个信息源时，通常是在每个州都在求主变量和转换级别上找到有关每个州的不一致或不完整的信息。 本文旨在将Belnap的四个值汇集在一起，即动态逻辑和混合机械，例如名义和满意度运算符，因此面对矛盾的证据，仍然可以推理。通过终止，声音和完整的tableaux系统探索了这种新逻辑的证明理论。
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.
