随着计算机技术的飞速发展,软件开发形式趋于多样化,同时软件的规模和复杂性也持续增长。面对层出不穷的软件质量问题,保证系统的安全性和可信性尤为重要。在此背景下,形式化验证方法作为一种以数学为理论支撑的技术,越来越广泛地应用于各种软、硬件安全特性的验证中,并逐渐成为各领域研究人员保障软件系统正确性和可靠性的重要方法。定理证明是形式化验证的重要手段之一,它基于严格的数学基础进行可靠的验证,在一定程度上弥补了模型检测的不足。同时,在使用定理证明方法对系统及性质进行描述和验证的过程中,使用的逻辑表达能力越强,能够描述和验证的系统性质越多。带索引表达式的命题投影时序逻辑（PPTLI）具有着完全正则的表达能力,与其它时序逻辑相比,PPTLI更适用于描述和刻画计算机程序和系统的各类性质。因此,使用一种表达能力更强的时序逻辑来开展定理证明工作有利于对更大规模系统的设计与性质验证。结合以上背景,本文以带索引表达式的命题投影时序逻辑PPTLI为主要研究对象,基于原型验证系统（PVS）开发了一套PPTLI半自动定理证明系统。本文的研究内容主要包括如下三个方面。（1）基于PVS的基本时序构造的证明系统的开发。首先,通过PVS规约语言对PPTLI中基本类型、基本时序操作符以及基本逻辑公式进行构建。然后,设计辅助规则来对状态公式进行约束,并对系统推理形式进行设计。在此基础上,通过PVS完成对基本时序构造的证明系统中的公理、推理规则的形式化描述。（2）基于PVS的索引表达式构造的证明系统的开发。首先,在完成对基本索引项类型以及无穷或操作符的类型构建的基础上,设计了一系列索引项类型间的连接词,并通过辅助公理来保证索性项类型与PPTLI类型间的正确转换。然后,设计了一种复杂索引表达式用于等价表示线性时序逻辑中的逻辑构造。最后,根据以上定义,通过PVS完成对索引表达式构造的证明系统中公理和推理规则的形式化描述。（3）定理实例的证明。通过本文开发的证明系统,对PPTLI中一系列具有典型性质的定理实例进行理论推导和交互式证明,主要包括了基本时序构造的定理以及索引表达式构造的定理。实例运行结果表明,本文构建的证明系统能够完成对复杂定理的描述和证明,并在定理证明过程中,呈现出良好的性能。