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?  

Numbers or Symbols?

I start this Blog with a reference to Pau Wilmott's Blog Numbers People and Symbols People. Paul is one of the most influencing quantitative analysts, in his blog he discusses the ability of people to handle abstractions.

But let me go back. When I studied Math in the early 70ies, I learned already about Symbolic Computation. In SC computers shall be able to manipulate and operate symbols, like mathematical expressions, geometrical objects, molecule structures or even programs. To manipulate and operate symbols needs a special language, the language of Mathematics. If you think of questions like "for all N, is there a K, so that sum (i, 1, 2, ..., N) = K?", the answer is "yes, K=N*(N+1)/2". If you do not want to verify this  across infinite many cases you ned a proof. This part of mathematics has to do with Quantifier Elimination. Solutions are in close form, if all quantifiers are eliminated. Close form solutions are exact and convenient. BUT, they usually only describe a small world. 

SC systems I used at that time: Mathematica, Maple, Macsyma, Derive, ... I was responsible for factory-automation software at Austria's largest industry enterprise and prototypically applied them in  robot and CNC programming and simulation.

1990, I met Stephen Wolfram, when he was on a world tour and I co-organized a talk in front of 400 people at the University of Linz. Fortunately I found out quickly that Stephen's Mathematica is the (only) adequate implementation of the language of mathematics with a declarative layer for programming and a representation of all symbols in unified expressions for unambiguous evaluation.

At this time, I launched my own company with the objective of creating innovative solutions on top of Mathematica.

But as mentioned, many problems cannot be transformed into closed form solutions. They need to be treated numerically. Good numerical schemes fit well along domains where close form solutions are available and do not lose this accuracy and robustness  "in between". MathConsult (Andreas Binder, CEO) is renowned for accurate and robust numerical solutions of the most complex technical problems.

When such numerical schemes are integrated into Mathematica, the solution inherits from Matematica its full declarative environment, visualisation, link technologies, ... and Mathematica's functionality is extended. UnRisk is such a solution.

So, it is Numbers AND Symbols. I will come back to this AND-effect.

Co^2-evolution

Mathematica is the system in which Wolfram|Alpha is implemented. It could not have a more solid foundation.

In my History of Future topic, I touched a few things about declarative programming (Mathematica's unambiguous language) and Quantifier Elimination a fundamentally mathematical technique to answer questions computationally. Is-there ...? yes-it-is-and-it-behaves-like-this....!

Wolfram|Alpha robustly supports free-form linguistic input and serves as knowledge engine. Mathematica's general symbolic language gives the framework of the knowledge representation and its vast built-in solvers provide the computational foundation. I always liked Mathematica-the-platform. And the Wolfram|Alpha Web Service API makes itself also platform. Call it from your programs.

So, a Mathematica program might call W|A that calls Mathematica. This might drive a co-evolution of new requirements and computational knowledge representation.

In How the Tablet Will Change The World (Wired), Steven Levy finds always-on tablet devices will blaze a path of future computing. In fact, they aim to make operating systems nearly invisible, to download and run useful daily apps, but also access power applications in the cloud.

Wolfram|Alpha on iPad let W/A go, where you go and again drives co-evolution of new requirements and .. the co^2-evolution.

Artificial Intelligence and Natural Stupidity

Again, a Blogtitle from Emanuel Derman's Blog. It links to an NY Times article, A First Church of Robotics , by Jaron Lanier.
One of the key characterizations in the article: technology is essentially a form of service (suggesting, IMO, shall be nothing else than ....). We work to make the world better ...  and bring more beauty into the world ...
I don't agree with this. I rather see the chance of co-evolution. 
Technology might help me to transform knowledge into margins or aesthetics. But it can also drive me to understand the nature of margins and aesthetics better. We might use our brain different, when communicating with another intelligence?
Intelligence is a huge subject, I do not want to discuss here, but Math Plugged touches mathematical intelligence, and why it would be quite poor without computers?


We thought computers are strong in algorithmic math whilst we re unbeatable in axiomatic math. But symbolic computation, automated theorem proving, quantifier elimination, ... show that this is not true any longer. OK, this might be still not be intelligence, associated to the idea of consciousness, ..... but enough to prevent me from doing stupid things (human proofs are often made with a nice taste, and even, if they are flawed, if widely accepted they are pushed into the mathematical knowledge base).


How will I use my brain during my little sessions with Wolfram|Alpha, now and in 5 years?

Mary, Mary, Quite Contrary

In Eliminate Quantifiers, I wrote about George E. Collin's Quantifier Elimination for real closed fields. The method he introduced is Cylindrical algebraic decomposition (cad).

It is a major concept of symbolic computation and theoretically it could be applied to collision detection (see One Size Fits All? briefly mentioning the application of the Simplex algorithm to collision detection).   But the complexity of cad is enormous.