公开宣告逻辑被广泛用于刻画在公开交流中知识的变化的推理问题,然而,公开交流下知识的表示和推理往往是复杂而多变的,虽然PAL语义一定程度上刻画了宣告行为引起的知识变化,但面对复杂的知识推理,需要一个更容易把握证明内定理思路的推演系统。一个可行的解决方案是构造公开宣告逻辑的带标的矢列演算系统,然而现有的G3PAL和GPAL都不同程度的存在一些问题。本文在总结前人研究的基础上,结合“语境依赖”语义构造新的PAL矢列演算系统G3PALC。首先表明G3PALC能够证明某些G3PAL中不能证明的内定理,并且G3PALC不需要针对宣告组合公理添加额外的规则。另外,G3PALC相对于GPAL而言,不需要添加相应的关系表达式规则,并且能够不借助引理直接证明宣告组合公理,同时G3PALC还具有GPAL所不具有的G3型系统特点,即收缩规则和弱化规则在系统内都是可允许的。最后我们证明G3PALC与HPAL和GPAL系统之间的等价性,以及语境依赖语义与删除世界语义和删除关系语义的等价性。本文结构安排如下:第一章:前言部分,介绍研究背景和研究现状。第二章:对公开宣告逻辑的标准语义和公理化系统HPAL进行介绍,并简述HPAL证明可靠性和完全性的一般方法。第三章:介绍公开宣告逻辑已有的矢列演算系统G3PAL和GPAL,并对两者的优缺点进行讨论。第四章:在G3PAL和GPAL的基础上,依据语境依赖语义构造公开宣告逻辑的矢列演算系统G3PALC,指出它相对于G3PAL和GPAL的优势,并证明它的可靠性和完全性,它与G3PAL和GPAL的等价性,以及语境依赖语义与标准语义和删除世界语义的等价性。