动态逻辑（模态逻辑）

在逻辑学、哲学和理论计算机科学中，动态逻辑是模态逻辑的一个扩展，能够对计算机程序的属性进行编码。这说明，如果地面目前是干的，而下雨了，那么之后地面就会是湿的。动态逻辑的语法包含一种命题语言（比如地面是干的）和一种行动语言（比如下雨了）。核心模态结构是(做一个动作零次或多次)。命题语言支持布尔运算（and,or,andnot）。行动逻辑有足够的表现力来编码程序。对于一个任意的程序{displaystylevarphito[P]varphi'}编码程序的正确性。编码程序的正确性，使动态逻辑比Hoare逻辑更通用。除了用于程序的形式化验证外，动态逻辑还被应用于描述语言学、哲学、人工智能和其他领域中出现的复杂行为。

模态逻辑的特点是模态运算符动态逻辑允许从较小的行动中建立起复合行动。虽然任何编程语言的基本控制运算符都可以用于这一目的，但Kleene的正则表达式运算符与模态逻辑很匹配。给定动作

这些运算符可以在动态逻辑中被公理化，如下所示，考虑到已经给出的合适的模态逻辑公理化，包括上述的模态运算符的公理。