Automated Computing, Solving, Proving:
A Key to the Information Age

Bruno Buchberger
RISC (Research Institute for Symbolic Computation)
University of Linz, Austria

Talk at the Presentation Day 
of the Computer Science Department 
of the University of Tsukuba, Japan
 February 24, 2003.

Copyright Bruno Buchberger 2003.

Copyright Note:  This file may be copied and stored under the following conditions:

         - the file is kept unchanged and includes the copyright note
         - a message is sent to buchberger@risc.uni-linz.ac.at
         - if the material is used then this talk should be cited appropriately.

A View on the Information Age

Dreamware

The desired objects should satisfy desired properties ("constraints").

For constructing the desired objects one has to know something about the world.

Knowledge, in a first stage, is obtained by observation: "Natural Sciences".

The individuals and the society have more and more complicated desires.

Natureware

Nature provides processes how to process information (representations of the "world").

These processes can be combined to "universal" (programmable) information processing machines: "The Computer".

A great invention of the 20 th century.

Deeper and deeper phenomena of nature are used for realizing the universal computer:
mechanical processes -> .... ->  biological processes ...

Mathware

The gap between the dreams and the universal machines becomes bigger and bigger.

The gap should be bridged "automatically": Specify the dream, press a button, and get fulfillment.

The gap is closed by "mathware"  (reasoning, mathematics, software science, ...):

model and explore (reason about) the world 
in a language which is close to the world
(a problem independent step)

specify the dream, propose a solution and prove that it is correct
(problem specific step)

translate, automatically, the language of dreams 
into the language of natureware
(a problem independent step).

Self-Application

Automation accelerates, deepens and widens by self-application.

Deeper knowledge about the "world".
The world becomes a "field" with only a few guiding principles (e.g. the "grand unification" of physics).

Better "natureware". 
Natureware becomes a global "field".

Better "mathware".
Mathware becomes automated "reasoning" on a very abstract and very concrete level.

Mathware: Automated Reasoning

Reasoning: Language, Reasoning Rules, Theories

A language consists of expressions that have meaning in certain "worlds".

Reasoning: step-wise transformation of expressions according to rules. ("Abstractness")

Reasoning rules:

Must preserve meaning.  ("Correctness")

Must be computer-executable.  ("Verifiability")

Theories: Collections of expressions.

Universal reasoning rules: correct in the empty theory. (Example: "Arbitrary but fixed".)

Special reasoning rules (for theory a T): correct, if one assumes T. (Example: Induction.)

Reasoning: Computing, Solving, Proving

Reasoning comes in three flavors: computing, solving, proving.

Computing (more generally, simplifying) in theory T:

Simplify[ expression, variable, knowledge–base]

The following must be valid in T⋃knowledge–base:

(Underscript[∀ , variable]) (expression  = 
          Simplify[ expression, variable, knowledge–base])

Simplifying processes  " (Underscript[λ, variable]) expression ".

Solving in T:

Solve[ expression, variable, parameter, knowledge–base]

The following must be valid in T⋃knowledge–base:

(Underscript[∀ , parameter]) Substitute[ expression, 
        variable,   Solve[expression,  variable,  parameter,  
          knowledge–base]]

Solving processes  " (Underscript[∃ , variable]) expression ".

Proving in T:

Prove[ expression, variable, knowledge–base]

If Prove[ expression, variable, knowledge–base] yields "proved", the following must be valid in T⋃knowledge–base:

(Underscript[∀ , variable]) expression

Proving processes  " (Underscript[∀ , variable]) expression ".

Reasoning: is a network of proving, solving, simplifying (computing).

Reasoning rules reduce 
            proving in T to solving and simplifying (in other theories)
            solving in T to proving and simplifying (in other theories) 
            simplifying in T to proving and solving (in other theories).

Example: Resolution theorem proving reduces proving to simplifying (clause form) and solving (unification).

Some Personal Interests

Theorema

Theorema (BB and Theorema Working Group 1996 - )  is a system in wich one should be able to

compute
solve
prove

in a uniform (logic and software) frame.

The logic is a version of predicate logic.

Gröbner Bases

Groebner Bases as a simplifier

The theory of Groebner bases (BB 1965 -), first, provides a simplifier:

Groebner–basis[F] gives a "standard form" for the polynomial ideal generated by F.

Example

GroebnerBasis[{x y z  -  3 (x^2) y + z + 1,  (x^2) y - x + 
          z - 1,  (x^2) + y z + (z^2)}, {z, y, x}]

The three new polys don't look "simpler" but, at least, they are "=" to the initial ones (in the theory of "polynomial ideals").

Hence, "Groebner-basis" is a simplifier.

However, Groebner bases can do a lot more: Solving and proving (and ...).

Reduce Solving (in the Theory of Complex Numbers) to GB Simplification

Solving: completely solving the three simultaneous polys is reduced to solving a unary poly and then, recursively, solve the others. (This needs a proof.)

Solve[-4 - 6 x + 4 (x^2) + 4 (x^3) - 12 (x^4) + 18 (x^5) + 
          29 (x^6) == 0]

This, again, does not look simpler but, algebraically, it is a good solution (compare (Sqrt[2]) !):

Simplify[-4 - 6 x + 4 (x^2) + 4 (x^3) - 12 (x^4) + 18 (x^5) + 
          29 (x^6) /. {x -> 
            Root[-4 - 6 #1 + 4 #(1^2) + 4 #(1^3) - 12 #(1^4) + 
                  18 #(1^5) + 29 #(1^6) &, 1]}]

A Starting Point for Numerical Solving

If you are not happy with this, then do it numerically:

NSolve[-4 - 6 x + 4 (x^2) + 4 (x^3) - 12 (x^4) + 18 (x^5) + 
          29 (x^6) == 0]

Now, you can substitute each of these solutions into the other polys of the Groebner basis:

{-4 - 6 x + 4 (x^2) + 4 (x^3) - 12 (x^4) + 18 (x^5) + 29 (x^6), 
        1178 - 1804 x - 4612 (x^2) + 2620 (x^3) - 1444 (x^4) - 10643 (x^5) - 
          1048 y, -84 - 362 x - 434 (x^2) - 262 (x^3) - 252 (x^4) - 
          1247 (x^5) + 
          262 z}  /. 
{x -> -0.9697048816586646`}

Solve[4050.339160494369` - 1048 y == 0]

In One Stroke

solutions = 
      Solve[{-4 - 6 x + 4 (x^2) + 4 (x^3) - 12 (x^4) + 18 (x^5) + 
              29 (x^6) == 0, 
          1178 - 1804 x - 4612 (x^2) + 2620 (x^3) - 1444 (x^4) - 
              10643 (x^5) - 1048 y == 
            0, -84 - 362 x - 434 (x^2) - 262 (x^3) - 252 (x^4) - 
              1247 (x^5) + 262 z == 0}]

solutions // N

The Solve Function of Mathematica (and Other Systems) Uses Groebner Bases

Solve[{x y z  -  3 (x^2) y + z + 1 == 
          0,  (x^2) y - x + z - 1 == 0,  
        (x^2) + y z + (z^2) == 0}]

In fact, what is done internally if you call the Solve function of Mathematica, is exactly the above Groebner bases computation plus back substitution.

Also note that the output of this "computation", is actually an algorithm how to obtain the solutions!

Reduce Proving (in the Theory of Complex Numbers), by Simplifying, to Solving and then to Simplifying

Implemented in Theorema: It yields the proof with explanatory text that explains the reduction method (every time it applies it).

Before this, Theorema must be loaded.

Now,

Formula["Boolean of Equalities",any[x, y],
	 ({{\(\((\ \ \((\(x\^2\) y - 3  x\ )\) ≠ 
                    0)\) ∨ 
\((\((x\ y + x + 
                        y)\) ≠ 
                    0)\) ∨ 
\ \ \ \ \ \((\((\((\(x\^2\) y + 3  x = 
                            0)\) ∨ \((\((\(-2\)\ x\^2 + \(-7\)\ x\ y + 
                                x\^2\ y + 
                                x\^3\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2 + 
                                2\ x\^2\ y\^2)\) = 
                            0)\))\)
	 ∧ \((\((x\^2 + \(-x\)\ y + 
                            x\^2\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2)\) = 
                        0)\))\)\),           "B1"}})]

Prove[Formula["Boolean of Equalities"], using -> {}, 
      by -> GroebnerBasesProver]

The Proof Completely Automatically Generated by the Groebner Bases Prover of Theorema

The PCS Prover

For Finding Proofs Involving Notions Defined by "Alternating Quantifiers"

Definition[\("limit:", any[f, a], 
	
      limit[f, a]⟺\ \(\(∀ \+ϵ\)\+\(ϵ > 0\)\(∃ \+N\(\(∀ \+n\)\+\(n ≥ N\)\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ\)\)\)\)]

Proposition[\("limit of sum", 
      any[f, a, g, 
        b], 
	\((limit[f, a] ∧ 
            limit[g, b])\)\ \ \ \ \  \[Implies] \ \ \ \ \ limit[f + g, 
          a + b]\)]

Proving, Computing, Solving as Explicit Phases in Proving

The PCS-method (BB 2002 - ):

P-phase: apply the typical inference rules for predicate logic (except the ones preserved for C- and S-phase).

C-phase: apply the typical inference rules for equalities, equivalences, implications (a kind of "symbolic computation" or "rewriting").

S-phase: solve in a "lower" theory.  (Solving may again include a P-phase, and so on.)

Knowledge Base

Definition[\("+:", 
      any[f, g, x], 
	\((f + g)\)[x] = f[x] + g[x]\)]

Lemma[\("|+|", 
      any[x, y, a, 
        b, δ, ϵ], 
	\((\[LeftBracketingBar]\((x + 
                    y)\) - \((a + 
                    b)\)\[RightBracketingBar] < \((δ + ϵ)\))\)\ \ \ \ ⟸\ \ \ \((\[LeftBracketingBar]x - a\[RightBracketingBar] < δ ∧ \[LeftBracketingBar]y - 
                  b\[RightBracketingBar] < ϵ)\)\)]

Lemma[\("max", any[m, M1, M2], 
	
      m ≥ 
          max[M1, M2]\ \ \ \ \  \[Implies] \ \ \ \ \ \((m ≥ 
              M1 ∧ m ≥ M2)\)\)]

Theory["limit",
	({{Definition["limit:"]}, {Definition["+:"]}, {Lemma["|+|"]}, {Lemma["max"]}})]

Proof (Generated Completely Automatically)

Prove[Proposition["limit of sum"], 
      using -> Theory["limit"], by -> PCS]

The Proof Completely Automatically Generated by the PCS Prover of Theorema:

Linear Boundary Value Problems

Brief Introduction

Boundary value problems for differential equations are of utmost imporatance for physics.

Extensively studied by numerical analysis.

Symbolic methods available only for very special classes: It is hard to get closed form for the differential equation that can then be fitted to the boundary conditions (and also show the dependence of the solution on the right-hand side of the differential equation).

New Symbolic Approach

New idea (M. Rosenkranz, BB, H. Engl, 2002) based on an earlier idea by W. Helton et al. 1998:

Represent both the differential equation, the right-hand side, and the boundary conditions as suitable operators in a Banach space.

All these operators are built up from some atomic operators in the form of non-commutative polynomials in the atomic operators. (These atomic operations reflect what you consider to be "available" operations!)

Then the boundary value problem can be expressed (by using the technique of the oblique More-Penrose equations) as non-commutative polynomial equations.

These equations can then be solved by a non-commutative version of the Groebner bases method.

At this moment, the method is worked out and implemented (within Theorema) for Ordinary Differential Equations and Linear Boundary Value Problems.

Green Function

Well-known Theorem:

Representation of the solution G of a BVP by Green function, depending on the right-hand side f:

(G (f)) (x) = (∫_a^b) g (x, ξ) 
          f (ξ) \[DifferentialD]ξ,

g is a "Green function" that depends on the left–hand side of the differential equation and the boundary values.

Example: Heat-Conduction in a Homogeneous Rod

Given f, find u such that:

u'' = f, 
u (0) = u (1) = 0.

In operator translation: G is the unknown operator in

(D^2) u = f, 
L u  =  
      0, 
R u  =  0,

where D is the derivative operator and

(L u) (x) = u (0),   (R u) (x) = 
      u (1).

Equalities for the Operators Using the More Penrose Equalities

(D^2) G (D^2)  =  (D^2), 
G (D^2) G   =  
      G, 
G (D^2)  =  
      1  - (1 - X) L - X R, 
(D^2) G  = 
      1,

where

(X u) x  =  x u (x).

Adding Equalities for antiderivatives we have, in addition:

D X  =  X D  + 1, 
D A  =  
      1, 
A D  =  
      1  -  L, 
D B   =  -1, 
B D  =  R  -  1, 
R X  =  
      R, 
L X  =  0,

where

(A u) x  =  (∫_0^x) 
          u (ξ) \[DifferentialD]ξ,    (B u) x  =  (∫_x^1) u (ξ) \[DifferentialD]ξ.

Apply Non-commutative Version of Groebner Basis Algorithm

We obtain a system of 41 polynomials, one of which has G "eliminated" (i.e. expressed in terms of known operators):

G  =  (X - 1) A X  +  
        X B (X  -  1).

This yields that

(G (f)) (x) = (∫_0^1) g (x, ξ) 
          f (ξ) \[DifferentialD]ξ,

with

g (x, ξ) =  (x - 
              1) ξ      if  0 ≤ ξ ≤ 
        x ≤ 
        1, 
                         x (ξ - 1)     if  0  ≤ 
      x ≤ ξ ≤ 1.

Hence, completely automatically, by one application of the GB algorithm, we obtained a well-known but non-trivial theorem on boundary value problems!

Infinitely many other theorems can be generated in this way, some of them unknown so far, see paper.

Mathematical Knowledge Management

Bourbakism of 20th Century

All of Mathematics

Develop all of mathematics within one logic frame: first order predicate logic.

Develop all of mathematics form only one notion: ∈.

This goal was reached by the Bourbaki Group. This can be considered as one of the biggest achievements in the 20th century.

The Build Up of Mathematics

Mathematics was built up in layers.

Mathematics was built up "by hand".

The content is not systematically verified (and, as it stands, inconsistent).

Mathematics was built up in one fixed way.

The Bourbaki books do not "live".

No Computers

The word "computer" does not occur in Bourbakistic mathematics.

Bourbakism of 21st Century

All of Mathematics

Make all of mathematics accessible and "living".

Mathematics built up in layers.

Many different ways ("views") of building up mathematics are possible and interesting.

"Computer" is the Main Content

The word "computer" is (one of) the main notion(s).

Computer-mathematics a major branch of mathematics. (The final goal and the biggest challenge of mathematics.)

"Computer" is the Main Tool

After designing a layer, most of the contents should be built up by computerized reasoning.

Thus, building up mathematics should be automated. (It, hence, should be verified and consistent.)

The main emphasis goes into constructing the network of provers, solvers, and simplifiers (for the various) layers that generate and / or verify the contents of the layers.

Mathematical Knowledge Management

Build up, store, and make accessible, over the web,  and alive "all" mathematical knowledge.

This overall goal has many subgoals whose solution needs all the accumulated know-how of computer mathematics and software technology.

This project is only at the beginning (MKM 2001 at RISC, MKM 2003 at U of Bologna, MKM 2004 at U of Birmingham) and is pursued by a growing network of research groups throughout the world.