共 41 条
[11]
Yang L.(1978)On the decision problem and the mechanization of theorem-proving in elementary geometry Sci China 21 150-172
[12]
Yang L.(1990)The parallel numerical method of mechanical theorem proving Theo Comput Sci 74 253-271
[13]
Yao Y.(1984)Cylindrical algebraic decomposition I: the basic algorithm SIAM J Comput 13 865-877
[14]
Yao Y.(1984)Cylindrical algebraic decomposition II: an adjacency algorithm for the plane SIAM J Comput 13 878-889
[15]
Wu W. T.(2001)Simple CAD construction and its applications J Symb Comput 31 521-547
[16]
Zhang J. Z.(1991)Partial cylindrical algebraic decomposition for quantifier elimination J Symb Comput 12 299-328
[17]
Yang L.(2007)A class of mechanically decidable problems beyond Tarski’s model Sci China Ser A-Math 50 1611-1620
[18]
Deng M. K.(2001)A complete algorithm for automated discovering of a class of inequality-type theorems Sci China Ser F-Inf Sci 44 33-49
[19]
Arnon D. S.(1996)A complete discrimination system for polynomials Sci China Ser E-Tech Sci 39 628-646
[20]
Collins G. E.(2009)Optimal sublinear inequalities involving geometric and power means Math Bohem 134 133-149