非单调推理是人工智能领域中一类重要的常识推理,其中包含缺省逻辑、自认知逻辑等内容。自认知逻辑的稳定集和扩充可用于刻划主体(agent)的推理能力以及认知状态,是自认知逻辑重要的研究内容。本文给出了稳定集的一种等价表示方法,该方法可以比较简洁、统一地描述多自认知逻辑中的相关概念。在多自认知逻辑中,本文基于对主体之间认知能力的不同假设,提出了四种稳定集,讨论了它们之间的关系,并以一种稳定集为例,给出了其语义表示,并引入了相应的扩充概念。另外,文中也讨论了一种可以描述环境的扩充。自认知逻辑程序可以看成是自认知逻辑的一种简化,可以比较方便地用于推理。本文分别讨论了单主体和多主体的自认知逻辑程序。对于单主体的情形,给出了一种不动点语义,证明了它和完全Bonatti稳定集等价,并可以转化为扩展逻辑程序的回答集语义。对于多主体的情形,根据对主体认知情况的不同处理,提出了两类稳定集:P稳定集和广义稳定集。在给出了多自认知逻辑程序的三值语义模型后,证明了该语义是和广义稳定集相互对应的。而当三值语义简化为二值时,对应的是P稳定集。P稳定集可看成是自认知逻辑程序中稳定集的自然推广,而广义稳定集可看成是Bonatti稳定集的推广。对于有序逻辑程序,本文基于不动点原理,提出了处理优先序的新方法,统一了多种已有的回答集语义,得到了一类新的回答集语义。通过证明和举例详细比较了各种回答集语义之间的强弱关系,给出了它们在集合包含关系意义下的哈斯图,证明了各种回答集语义在包含关系下形成格的结构。安全协议是保证网络通信安全的重要内容。形式化方法是验证安全协议的一种重要方法。本文提出了一种复合型安全协议,在同一协议中结合了在线可信第三方和离线可信第三方两种通信方式。对SVO逻辑和Kailar逻辑进行扩充,增强其表达能力,特别是非单调推理能力,给出了协议验证的新方法。另外,作为逻辑程序的一种应用,本文也提出了基于多自认知逻辑程序的验证方法,并以KM等协议为例,验证了协议的非否认性和公平性等性质。