非Tarski模型定理机器证明

利用新近发展的自动发现不等式型定理的完备算法及差分代换算法等机器证明方法，结合对称多项式的Timofte降维方法，对几类Tarski模型外的不等式，包括系数或指数依赖于一个（甚至多个）离散参数的多项式不等式，这里的离散参数可以是一个不确定的自然数，以及一些积分不等式等，给出机器证明判定算法，当给定的不等式不成立时，尝试给出具体不成立的数值反例，从而实现对几类Tarski模型外的命题的机器证明或自动验证。上述Tarski模型外的不等式的特点与杨路等人最近发表在《中国科学》上的论文中提出的几个公开问题密切相关，是比较有代表性的一类机器证明问题。申请人已在上述几个方面进行了部分有益的探索，均得到令人满意的结果，有较强的研究基础。申请人已发表期刊论文五十余篇，其中《IEEE Trans.AC》及《IEEE Trans.CAS》六篇，《中国科学（中英文）》七篇。

利用新近发展的自动发现不等式型定理的完备算法及差分代换算法等机器证明方法，结合对称多项式的Timofte降维方法，对几类Tarski模型外的不等式，包括系数或指数依赖于一个（甚至多个）离散参数的多项式不等式，这里的离散参数可以是一个不确定的自然数，以及一些积分不等式等，给出机器证明判定算法，当给定的不等式不成立时，尝试给出具体不成立的数值反例，从而实现对几类Tarski模型外的命题的机器证明或自动验证。上述Tarski模型外的不等式的特点与杨路等人最近发表在《中国科学》上的论文中提出的几个公开问题密切相关，是比较有代表性的一类机器证明问题。申请人已在上述几个方面进行了有益的探索，得到令人满意的结果。项目期间已发表期刊论文十余篇，论文发表于《IEEE Trans. ITS》、《IET Control Theory & Applications》、《中国科学》及《智能系统学报》等。