随着形式化验证技术的应用与发展,定理证明和模型检测两种验证技术优势互补,在安全攸关系统（航空工业、探月工程、自动驾驶技术等）的验证上,发挥了越来越重要的作用。定理证明技术用演绎推理手段,对系统是否满足特定的安全性质进行严格的数学推导证明,已有多种基于定理证明的验证工具问世。然而,误差在系统中是普遍存在的,目前大部分基于定理证明的验证理论较少考虑系统中的误差参数。因此,针对含误差的安全攸关系统的形式化验证工作有重大的理论及现实意义。另一方面,多项式代数系统在描述连续数据交换、连续状态等方面有较强的刻画能力,此外近年来,多项式代数（符号计算的分支领域）也有长足的发展。例如:实根隔离算法、Gr（?）bner基、吴方法、半代数系统求解。正是基于以上思考,以及结合几年来在这一领域的持续研究,我们在以下几方面有所创新:（1）误差线性断言推理方法:证明了误差线性断言零点集为凸集,提出了求解误差线性断言顶点集的方法,并证明了该方法的正确性。经分析相关概念及定理,将判断误差线性断言之间的蕴含关系转化为前驱断言的顶点是否被包含在后驱断言的零点集的判断问题,从而给出了判断误差线性断言的蕴含关系的方法步骤。最后,将该方法应用在火车匀速和加速运动上,并用大量随机误差参数模拟验证了该方法的有效性。（2）非线性误差多项式断言推理方法:将误差多项式断言之间的蕴涵关系转化为它们零集之间的包含关系;将误差多项式断言转换为一阶多项式逻辑公式。研究结合基于柱形代数分解的量词消去方法,将误差多项式断言零点集之间的包含关系转化为特定一阶多项式逻辑上的量词消去问题。最后,以目标拦截问题的为例,通过大量随机误差参数验证了该方法的正确性。（3）结合误差概率信息的误差多项式断言推理方法:用截断正态区间来描述误差,部分地简化了截断正态区间的运算,提出了与误差的概率信息相结合的误差多项式推理方法。依据误差的统计学信息,我们的方法能更及时地判断出系统潜在的非误差故障。最后给出该方法在火车加速动力分配两体问题上的应用,经对其误差参数的大量测试,测试结果与理论推理结果一致。（4）在误差语义上,用区间和截断正态区间来刻画误差,分析了区间运算中存在的两个问题（不可逆性、范围扩大性）。本文推理方法（误差线性断言和非线性误差多项式推理方法、结合误差概率信息的推理方法）大大的避免了这两种问题。误差多项式断言是多项式代数断言的推广,当区间数的上界和下界相等时,误差多项式断言就退化为经典多项式断言,因此我们提出的误差多项式断言与经典多项式断言逻辑自洽。定义了误差多项式断言的零点集,并且同样做到了与经典多项式零点集自洽,并给出了误差多项式断言蕴含关系的等价条件。