经典的信念逻辑系统S_KD45只能表达主体某个静止状态的信念及推理,事实上,在收到新信息后,主体的信念将发生变化。动态认知逻辑是动态逻辑和认知逻辑相结合的结果,它为信息变化提供了一种形式化的处理方法。本文旨在建立一个能处理信念变化的信念修正逻辑系统S_DBR。第一部分:首先介绍经典的信念逻辑系统S_KD45,该系统能较好地刻画相信算子的性质:无矛盾性、正内省性、负内省性,同时指出它的不足——不能描述动作所产生的变化,也不能刻画多主体间的相互作用。接着介绍传统的信念修正理论——AGM理论,它虽然能反映主体信念变化的过程,但并不是一个形式化的系统。第二部分:为了将信念排序,首先介绍顺序条件函数,它可以处理当主体收到带一定牢固度的命题后信念是如何变化的。在此基础上,引入静态的信念逻辑系统S_SBR,给出语言、语义以及证明系统,最后给出完备性的证明。第三部分:在静态的信念逻辑系统S_SBR基础上,将行动模型在认知逻辑中的执行作为动态模态算子引入逻辑语言中,建立动态的信念修正逻辑系统S_DBR。由于S_DBR可以归约到S_SBR,所以可以证明S_DBR也是完备的。第四部分:对S_DBR做出评价,指出不足之处,并指明在未来需要进一步研究的问题。