Automated theorem proving on inequalities is always considered asa difficult topic in the area of automated reasoning. The relevallt algorithms dependfundamentally on real algebra and real geometry, and the computational complexityincreases very quickly with the dimension, that is, the number of parameters. Somewell-known algorithms are complete theoretically but inefficient in practice, whichcannot verify non-trivial propositions in batches. A dimension- decreasing algorit hmpresellted here can treat radic…

This article shows the recent developments on orthogonal draw-ings of graphs which have applications for the automation of VLSI circuit design.Meanwhile, a number of problems are posed for further research.

It is a famous result of Kempe that a lillkage can be designed togenerate any given plane algebraic curve. In this paper, Kempe's result is improvedto give a precise algorithm for generating Kempe linkage. We proved that for analgebraic plane curve of degree n, Kempe linkage uses at most O(n4) links. Effortsto implement a program which may generate Kempe linkage and simulation of thegeneration process of the plane curves are presellted in the paper.

Recently algorithms for solving propositional satisfiability problem,or SAT, have aroused great illterest, and more attention has been paid to trans-formation problem solving. The commonly used transformation is representationtransform, but since its ifltermediate computing procedure is a black box from theviewpoint of the original problem, this aPproach has many limitations. In this paper, a new approach called algorithm transform is proposed and applied to solvingSAT by Wu's method, a general algorithm fo…

In this paper, the possibility of fast algorithm is discussed for me-chanical theorem proving, where the degeneracy condition are considered in designingof these algorithms. It is found that all of the methods depend seriously on some prin-ciples appearing in Wu's Method. In other words, some principles in Wu's Methodare the instinctive properties in these new fast algorithms of theorem proving.

ELIMINO is a mathematical research system developed for theimplementation of Wu's method, a powerful method for polynomial equation systemsolving and geometric theorem proving. The aim of ELIMINO is to provide usera programmable interpreting environment to use Wu's method in scientific researchand engineering computation. In this paper, the development of ELIMINo systemis outlined and the techniques adopted are discussed, then some details about theobject-oriented analysis of ELIMINO are presented.

A new type of intelligent CAI system for chemistry is developed inthis paPer based on automated reaJsoning with chemistry knowledge. The systemhas shown its ability to solve chemistry problems, to assist students and teachersin studies and instruction with the automated reasoning functions. Its open modeof the knowledge base and its unique style of the illterface between the system andhuman provide more opportunities for the users to acquire living knowledge throughactive participation. The automated reason…

This article deals with the structure relations between solutions toalgebraic system and matrices in eigenvalue method for solving the algebraic system-The authors first discuss the condition on the ideal generated by the given systemunder which the eigenspace of matrix has dimension 1 since in this case the zerocan be easily found. Then they study the relations between the multiplicity of zerosof the given system and orders of Jordan blocks of matrices formed in eigenvaluemethod.

one of the central questions in CAGD[1] is blending surfaces whichprovides the theoretical baJsis for the design technology of space surfaces. We willdiscuss the general theories and algorithms for multivariate hyperfinite interpolationand their aPplication to the blending of implicit algebraic surfaces, and investigate theexistence conditions of hyperfinite interpolation. Based on Wu's theory on blendingimplicit algebraic surfaces, the problem of blending two quadric surfaces is studied.The conditions for …