Examples of RISC Research

B. Buchberger.
Appendix of talk at Symposium "Mathematics and New Technologies: How to Learn? What to Teach?", Dec 10-11, 2003, Madrid.

Groebner Bases: Well Established in Research and Systems

BB's Groebner bases method is implemented in all current math software systems for all problems involving multivariate polynomials. For an overview see

B. Buchberger. Introduction to Groebner Bases.
In: Groebner Bases and Applications (B. Buchberger, F. Winkler, eds.),
Cambridge University Press, 1998, pp.3-31.

F = {x (y^2) - 3  x y + 2, (x^2) y - 5 (x^2) - 2  x y  + 
          3}

GroebnerBasis[F]

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

Symbolic Summation: Well Established in Research

Zeilberger, Paule, ... method. Based Groebner bases for non-commutative polyonomials play a role.

Example: Closed form for the following expression was an open problem for many years! The solution was given in P. Paule,  Computer-Solution of Problem 94-2, SIAM REVIEW Vol.37 (1995), 105-106 using the Paule-Schorn automated conjecture generator / prover.

The method is not yet routinely available in math software systems.

Formula[\("SIAM series", 
	∑\+\(k = 1, …, n\)\(\(\((\(-1\))\)\^\(k + 1\)\) \((4\ k + 1)\) \(\((2\ k)\)!\)\)\/\(\(2\^k\) \((2\ k - 1)\) \(\((k + 1)\)!\) \(2\^k\) \(k!\)\)\)]

Simplify[Formula["SIAM series"], 
      by -> PauleSchorn–Telescope, 
      built–in -> Built–in["PauleSchorn"]]

Automated Proving in Elementary Analysis: Under Study

The PCS prover (BB 2000): Experimental implementation in the frame of the Theorema system.  See

B. Buchberger.
The PCS Prover in Theorema.
In: R. Moreno-Diaz, B. Buchberger, J.L. Freire (eds.), Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), Feb. 19-23, 2001, Las Palmas de Gran Canaria,  Lecture Notes in Computer Science 2178, 2201, Springer, Berlin - Heidelberg - New York, pp. 469-478

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]\)]

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"]}})]

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

By this Theorema call, the following proof is generated completely automatically by our PCS proving algorithm:

Automated Algorithm Invention by Failing Correctness Proofs: On the Horizon

Recent research (BB 2002) with some encouraging results, see

B. Buchberger.
Algorithm Invention and Verification by Lazy Thinking. 
In: D. Petcu, V. Negru, D. Zaharie, T. Jebelean (eds), Proceedings of SYNASC 2003 (Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 1-4, 2003), Mirton Publishing, ISBN 973-661-104-3, pp. 2-26.

Give a problem specification, e.g. find 'sort' such that

(Underscript[∀ , is–tuple[X]])is–sorted–version[X, 
        sorted[X]]

where

(Underscript[∀ , is–tuple[X]])(is–sorted–version[X, Y]  ⇔{({{is–tuple[Y] }, {X≈Y  }, {is–sorted[Y]}})}).

Press the button and get algorithms for the problem:

(Underscript[∀ , is–tuple[X]])(sorted[X]={({{special[X], ⇐, is–trivial–tuple[X]}, {merged[sorted[left–split[X]], 
                    sorted[right–split[X]]], ⇐, otherwise}})})

and

sorted[⟨⟩] = c

(Underscript[∀ , x])(sorted[⟨x⟩] = 
          d[x])

\(∀ \+\(x, y, z\&_\)\((sorted[⟨x, y, 
              z\&_⟩] = 
          i[x, sorted[⟨y, 
                z\&_⟩]])\)\)

and

...

Note after the conference: A major step forward was achieved by this method in Jan 2004, see

B. Buchberger.
Towards the Automated Synthesis of a Gröbner Basis Algorithm.
RACSAM (Rev. R. Acad. Cien. Serie A. Mat.), 10 pages, submitted.

In this paper I show that, with my above 2003 algorithm synthesis method, it is possible to automatically synthesize the Groebner bases algorithm illustrated in the first section above. This shows that the 2003 synthesis method is strong enough to synthesize also highly non-trivial algorithms.