复系数质点法是以几何点的运算为基础而建立起来的一种新的几何定理机器证明方法.它能高效地证明大部分构造型几何命题,但现有的复系数质点法仍不能有效地处理一些非线性构造型几何命题.为此,该文在原有工作的基础上,对原复系数质点法...复系数质点法是以几何点的运算为基础而建立起来的一种新的几何定理机器证明方法.它能高效地证明大部分构造型几何命题,但现有的复系数质点法仍不能有效地处理一些非线性构造型几何命题.为此,该文在原有工作的基础上,对原复系数质点法机器证明算法进行了较大的改进,新添加了一些重要的构图方式,并选用Mathematica重新实现了改进的算法,创建了新的证明器CMPP(Complex Mass Point method Prover).对上百个几何定理的运行结果显示,证明器CMPP能有效地处理非线性构造型几何命题以及许多非构造型几何命题,在解题能力及运行效率上均有所提高.特别地,CMPP能在短时间内实现五圆定理、莫莱定理等一些难度较大的几何定理的可读机器证明.展开更多
This paper develops fuzzy H∞ filter for state estimation approach for nonlinear discretetime systems with multiple time delays and unknown bounded disturbances. We design a stable fuzzy H∞ filter based on the Takagi...This paper develops fuzzy H∞ filter for state estimation approach for nonlinear discretetime systems with multiple time delays and unknown bounded disturbances. We design a stable fuzzy H∞ filter based on the Takagi-Sugeno (T-S) fuzzy model, which assures asymptotic stability and a prescribed H∞ index for the filtering error system. Sufficient condition for the existence of such a filter is established by solving the linear matrix inequality (LMI) problem. The LMI problem can be efficiently solved with global convergence using the interior point algorithm. Simulation exanples are provided to illustrate the design procedure of the proposed method.展开更多
After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable ...After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.展开更多
基金National Natural Science Foundation of P. R. China (60084002 and 60174018) National Key Project for Basic Research of P. R. China ( G2002cb312205) +1 种基金 National Excellent Doctoral Dissertation Foundation of P. R.China (200041) and National Natural Sci
基金Supported by National Natural Science Foundation of P. R. China (60174028) and 10th Five-Year Armament Pre-research Foundation of P. R. China (BZJ040202)
文摘复系数质点法是以几何点的运算为基础而建立起来的一种新的几何定理机器证明方法.它能高效地证明大部分构造型几何命题,但现有的复系数质点法仍不能有效地处理一些非线性构造型几何命题.为此,该文在原有工作的基础上,对原复系数质点法机器证明算法进行了较大的改进,新添加了一些重要的构图方式,并选用Mathematica重新实现了改进的算法,创建了新的证明器CMPP(Complex Mass Point method Prover).对上百个几何定理的运行结果显示,证明器CMPP能有效地处理非线性构造型几何命题以及许多非构造型几何命题,在解题能力及运行效率上均有所提高.特别地,CMPP能在短时间内实现五圆定理、莫莱定理等一些难度较大的几何定理的可读机器证明.
基金国家自然科学基金，Natural ScienceFoundation of Liaoning Province P.R.China
文摘This paper develops fuzzy H∞ filter for state estimation approach for nonlinear discretetime systems with multiple time delays and unknown bounded disturbances. We design a stable fuzzy H∞ filter based on the Takagi-Sugeno (T-S) fuzzy model, which assures asymptotic stability and a prescribed H∞ index for the filtering error system. Sufficient condition for the existence of such a filter is established by solving the linear matrix inequality (LMI) problem. The LMI problem can be efficiently solved with global convergence using the interior point algorithm. Simulation exanples are provided to illustrate the design procedure of the proposed method.
基金supported by the Funds of the Chinese Academy of Sciences for Key Topics in Innovation Engineering under Grant No.KJCX2-YW-S02
文摘After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.
