Automated methods for formal proofs in simple arithmetics and algebra (Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren)

Automated methods for formal proofs in simple arithmetics and algebra (Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren)
复制标题

简单算术和代数形式化证明的自动化方法（Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren）

DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
A. Chaieb
A. Chaieb
中科院分区：
--
文献类型：
--
作者：
A. Chaieb

文献摘要

被引文献

相似文献

在LCF类定理证明器中，任何证明都必须从一个小的 推理规则集。自动证明方法的发展 这样的系统是非常重要的。在这篇论文中，我们研究了 问题：我们应该如何将证明程序纳入 LCF类定理证明器，无论是在一般情况下，还是在特殊情况下， 算术？我们研究了三种集成范式 并提出了几个证明程序。其中包括普遍性和弱 环上的存在性问题，环上的泛多项式问题 上参数线性问题的实量词消去 有序域，Presburger算法，混合实整数线性 算术的、代数的和真实的闭域。我们的工作得到 在伊莎贝尔框架内进行。
In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential problems over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework.