Eliminate Quantifiers

Later 80ies. I met George E Collins (University of Madison - cooperating with RISC). His research field: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. His research team developed a system. The objective: ask a question like "For all Circles C1 and C2, is there an intersection point P12 of C1 and C2?" and get an answer showing the conditions (no-1-2) and how to calculate (a closed form solution).

Mathematics is quantifier elimination? When you write an equation, you have in mind to solve it. And even if you do not explicitly ask it, you might have "Is there, so that ..?", "under conditions ?", with constraints ?", ... in mind. To answer such questions, you need an input interpreter, a mathematical knowledge base, a computational engine and a result reporter?

Over 20 years later, Wolfram has introduced Wolfram Alpha the computational-knowledge engine. Fruit of challenging research, a clear concept carried by a symbolic language to represent anything and the algorithmic power to do any kind of computation, Mathematica!, and massive data. And it takes questions people ask in natural language, suppressing the "Is there..?", "under conditions?", "which constraints?".... NOT a search engine. NOT a content representation. A computational-knowledge engine, If you want, a general quantifier eliminator?