Automated Proofs 
of Automated Geometry Provers

Bruno Buchberger
RISC (Research Institute for Symbolic Computation), Schloss Hagenberg, A4232 Austria

Invited talk at ADG 2002 (Automated Deduction in Geometry)
RISC, Schloss Hagenberg, A 4232 Austria
Sep. 4, 2002

Copyright Bruno Buchberger 2002.

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

-  the file is kept unchanged including the copyright note
- a message is sent to  buchberger@risc.uni-linz.ac.at
- if the material is used, please, cite the talk appropriately.

Overview

Automated geometry provers (based on algebraic algorithms)

Automated proofs of geometry provers

The transition from the object level to the meta-level

Automated Geo Provers

Correct Automated Provers

Algorithm      Prove–in–theory–T–by–method–M[ f, K]:

f ...  a formula from some class ℱ of formulae (in predicate logic)

K ...  a knowledge base (set of formulae from class ℱ)

T ...  underlying theory (set of formulae in predicate logic).

(Weak) Correctness Theorem:   If  Prove–in–theory–T–by–method–M[ f, K] yields a proof  
                                                    then  f must be a logical consequence of the axioms of T and K.

In geo proving, K is often empty.

Why is this reasonable? Why is K sometimes / often  important?

Example of an Implementation

In Theorema:

Formula["Test",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["Test"], using -> {}, 
      by -> GroebnerBasesProver]

Prove[ ... by->GroebnerBasesProver] is the algorithm name.

The theory T is hidden: theory of complex numbers.

Every individual proof automatically generated by this prover also "explains" the algebraic method behind the prover.

Correctness of this prover: based on Groebner bases theory.

Other implementations of geo prover based on algebraic methods (Wu, Collins, GB, ...): see this conference, talks by J. Robu, D.M. Wang, ...

The Proof Generated Automatically by the Theorema Groebner Bases Prover

Automated Proofs of Geo Provers

The Problem

(Weak) Correctness Theorem:   If  Prove–in–theory–T–by–method–M[ f, K] yields a proof  
                                                    then  f must be a logical consequence of the axioms of T and K.

How can we prove this?

By a proof produced individually by a mathematician. Done. See the literature.

By a proof produced  by an automated prover (which works for infinitely many theorems, e.g. correctness theorems). The prover has to be invented by a human mathematician.

This is the challenge. (See BB 1996, Proc. FROCOS 96).

In the case of a geo prover based on Groebner bases, the challenge is essentially the automated proof of the "main theorem":

Theorem[any[
        F], 
is–Groebner–Basis[
            F]⟺(Underscript[∀ , f, g ∈ F])remainder[S–polynomial[f, g], F] = 0]

Progress Made

This challenge was one of the motivations for designing and developing Theorema.

Solution in L. Thery 2001, A Machine-Checked Implementation of Buchberger's Algorithm, JAR 26, 107-137, 2001.

Solution in J.L. Ruiz-Reina et al. 2000, A Mechanical Proof of the Knuth-Bendix Critical Pair Algorithm, Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000), St.Andrews, Scotland.  TR   5-2000, Fachberichte Informatik, Universitat Koblenz-Landau, 2000.

Others ? See references in L. Thery 2001.

Literature

L. Thery

L. Thery gives a complete solution of the problem, i.e. the proof of (the relevant part of) GB is completely "mechanical".

In which sense?

Proofs of (the relevant part of) GB theory automatically checked by Coq.

Coq is based on type theory.

Algorithms defined in Coq can be automatically translated into Ocaml programs and can then be executed.

Build-up of the theory (polys, congruence, reduction, S-polys, main theorem, GB algorithm) follows closely my / the original papers on GB.

The intermediate lemmata and theorems and their proofs are formulated by the user and checked by the system.

Hence what was basically obtained is a mechanical detailed check of (the relevant part of) the existing proofs in the literature. The steps to be applied in the checking process must be described in "tactics".

In other words, instead of giving the proofs invented by a mathematician to a good student (or a good professor) for checking, one can give the proofs to Coq.

Part of the intermediate steps are mechanically produced by the tactics "Auto".

L. Thery reports:

14.000 lines of proof tactics to be written for checking the proofs (1000 lines for the actual GB algorithm).

1 1/2 years work.

"Work could benefit from more automation."

J.L. Ruiz-Reina et al.

They give a complete solution of a similar problem, namely the Knuth-Bendix critical pair theorem.

In which sense?

Proofs of (the relevant part of) are automatically generated by ACL2.

ACL2 evolved from Nqthm (Boyer-Moore theorem prover).

ACL2 is a quantifier-free fragment of predicate logic with =.  (No ∃ !)

ACL2 is also a programming language (close to Common Lisp).

Main proof tool: induction.

The individual proofs are generated completely automatically.

User support of proving activity: by formulating definitions and lemmata in a suitable order (using proved lemmata as new formulae in the knowledge base).

Build-up of the theory (terms, congruence, reduction, unification, critical pairs, cp theorem) follows closely the original papers.

The intermediate lemmata and theorems are formulated by the user and the proofs are generated by the system.

All lemmata have to be formulated (∃-) quantifier-free.

However, there are situations where essential invention goes into this kind of formulating lemmata. (The "solving terms" have to been invented by the user.)

The degree of automation in the generation of the proofs is much higher than in Thery's approach.

Readability is questionable.

The authors remark:

Very weak logic can be used to formalize and reason about non-trivial properties of equational reasoning.

As a byproduct, certified Common Lisp code is obtained for some basic algorithms used in rewriting theory (like subsumption, unification, reduction to normal form).

Theorema

Some Aspects of the Challenge

Much progress has been made but there is room for improvement.

"More automation":

Automated generation of proofs for formulae containing "∃", in particular "∀∃...".

Automated generation of proofs for formulae containing "{ ..| ..}"  (set theory).   
( Ideal[F] := { (∑_(i = 1)^m) (Subscript[h, i]) (Subscript[f, i]) | ...  (Subscript[f, i]) ∈  F ...} )

Invention of intermediate lemmata.

"More attractive":

"Readable" proofs.

Structured build-up of theory ("polymorphism").

Logic-internal execution of algorithms (algorithmic formulae).

Current State in Theorema

Most of the above issues are addressed (and solved to some extent).

They are not yet combined and integrated for a coherent and satisfactory solution of the original challenge.

Readability, Structure, Alternating Quantifiers

Example: Elementary Analysis

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

Automated Construction of Solving Terms, Readability

The "PCS" method: A heuristic proof method (BB 2000) for formulae involving alternating quantifiers

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

Proof contains interesting algorithmic and didactic information!

The Proof Generated Automatically by the Theorema PCS Prover

Set Theory

The Theorema set theory prover (PhD thesis of W. Windsteiger) is also based on the PCS principle.

Definition[\("reflexivity", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–reflexive\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x ∈ A\)x ∼ x\)\)\)]

Definition[\("symmetry", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–symmetric\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x, y ∈ A\)\((x ∼ y \[Implies] y ∼ x)\)\)\)\)]

Definition[\("transitivity", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–transitive\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x, y, z ∈ A\)\((x ∼ 
                    y ∧ y ∼ z \[Implies] x ∼ z)\)\)\)\)]

Definition["equivalence",any[∼,A],
is–(Subscript[equivalence, A])[ ∼ ]:⇔∧{({{is–(Subscript[reflexive, A])[ ∼ ]}, {is–(Subscript[symmetric, A])[ ∼ ]}, {is–(Subscript[transitive, A])[ ∼ ]}})} ]

Definition[\("class", 
      any[x, \(\(∼\)\(\(,\)\(A\)\)\)], 
class\_\(A,  ∼ \)[
          x] := {a ∈ A \[VerticalSeparator] 
            a ∼ x ∧ x ∈ A}\)]

Proposition[\("equal classes", 
      any[x ∈ A, y ∈ A, \(\(∼\)\(\(,\)\(A\)\)\)], 
      with[is–equivalence\_A[ ∼ ]], 
x ∼ y \[Implies] \((class\_\(A,  ∼ \)[x] = 
            class\_\(A,  ∼ \)[y])\)\)]

Prove[Proposition["equal classes"],
\(using -> ⟨Definition["equivalence"], 
            Definition["transitivity"], Definition["symmetry"], 
            Definition["class"]⟩\),
by -> SetTheoryPCSProver,
transformBy -> ProofSimplifier,TransformerOptions -> {branches -> Proved, 
              steps -> Useful},ShowOptions -> {},
\(ProverOptions -> {GRWTarget -> {"goal", "kb"}, AllowIntroduceQuantifiers -> True, 
              UseCyclicRules -> True, DisableProver -> {STC, PND}, 
              ApplyBuiltIns -> {}}\),SearchDepth -> 50]

Automated Invention of Intermediate Lemmata

Definition["addition",any[m, n],
	({{m + 0 = m, " +0:"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + .:"}})]

Proposition["commutativity of addition",any[m, n],
	({{m + n = n + m, " + = "}})]

Failing proof:

\(\(Prove[Proposition["commutativity of addition"], 
	
        using -> ⟨Definition["addition"]⟩, 
	by -> NNEqIndProver, 
	
        ProverOptions -> {TermOrder -> LeftToRight}, 
        transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> {Proved, 
                Failed}}];\)\)

Successful proof and  invention of additional knowledge by the "cascade":

\(\(Prove[Proposition["commutativity of addition"], 
	
        using -> Definition["addition"], 
        by -> Cascade[NNEqIndProver, ConjectureGenerator], 
        ProverOptions -> {TermOrder -> LeftToRight}];\)\)

The First Proof Generated by the Cascade

Pending proof of (1).

Pending proof of (18).

The Second Proof Generated by the Cascade

The Third Proof Generated by the Cascade

Pending proof of (1).

The Fourth Proof Generated by the Cascade

The Fifth Proof Generated by the Cascade

Polymorphism by Functors, Logic-Internal Execution of Algorithms

A Sparse Polynomials Functor

Definition["pol" ,any[C, T],
pol[C, T] =Functor[P,\(any[c, d, i, m\&_, n\&_, p, q, s, t]\),
	({{𝕤 = ⟨0 ∶ P, 
                        1 ∶ 
                          P, +∶P\[Cross]P -> 
                              P, -∶P -> 
                              P, -∶P\[Cross]P -> 
                              P, *∶P\[Cross]
                                P -> P⟩}, {({{
(Underscript[0, P]) = ⟨⟩}, {(Underscript[1, P]) = ⟨⟨(Underscript[1, C]), 
                                (Underscript[1, T])⟩⟩}, {\(⟨⟩\( + \+P\)q = q\)}, {\(p\( + \+P\)⟨⟩ = p\)}, {\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\( + \+P\)⟨⟨d, t⟩, 
                                n\&_⟩ = \[LeftDoubleBracketingBar]⟨c, 
                                    s⟩⌣\((⟨m\&_⟩\( + \+P\)⟨⟨d, t⟩, 
                                        n\&_⟩)\) ⇐ s\( > \+T\)t, 
	⟨d, 
                                    t⟩⌣\((⟨⟨c, s⟩, 
                                        m\&_⟩\( + \+P\)⟨n\&_⟩)\) ⇐ 
                                t\( > \+T\)s, 
	\((⟨c\( + \+C\)d, s⟩)\)⌣\((⟨m\&_⟩\( + \+P\)⟨n\&_⟩)\) ⇐ \((c ≠ \(-\+C 
                                      d\))\), 
\((⟨m\&_⟩\( + \+P\)⟨n\&_⟩)\) ⇐ 
                                otherwise\[RightDoubleBracketingBar]\)}, {\(\(-\+P⟨⟩\) = ⟨⟩\)}, {\(\(-\+P⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\) = ⟨\(-\+C c\), 
                                s⟩⌣\((\(-\+P⟨m\&_⟩\))\)\)}, {\(p\( - \+P\)q = p\( + \+P\)\((\(-\+P q\))\)\)}, {\(⟨⟩\(*\+P\)q = ⟨⟩\)}, {\(p\(*\+P\)⟨⟩ = ⟨⟩\)}, {\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\(*\+P\)⟨⟨d, t⟩, 
                                n\&_⟩ = \((⟨⟨c\(*\+C\)d, 
                                      s\(*\+T\)t⟩⟩\( + \+P\)⟨⟨c, 
                                        s⟩⟩\(*\+\(\(P\)\(\ \)\)\)⟨n\&_⟩)\)\( + \+P\)⟨m\&_⟩\(*\+\(\(P\)\(\ \)\)\)⟨⟨d, t⟩, 
                                  n\&_⟩\)}})}})
	]]

Theorema programs are just one special class of formulae!

Generate 3-Variate Polys over the Integers

Theory["F",
	({{Definition["integers"]}, {Definition["power products"]}, {Definition["pol"]}})]

Definition[\("D", 
	ℙ = 
        pol[integers[], power–products[3]]\)]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Theory["F"], Definition["D"]⟩]

\(Compute[\((⟨⟨5, ⟨2, 3, 
                1⟩⟩, ⟨3, ⟨1, 6, 
                3⟩⟩⟩\(*\+ℙ\)\((⟨⟨5, ⟨2, 3, 
                    1⟩⟩, ⟨3, ⟨1, 6, 
                    3⟩⟩⟩\(*\+ℙ\)⟨⟨5, ⟨2, 3, 
                    1⟩⟩, ⟨3, ⟨1, 6, 
                    3⟩⟩⟩)\))\)]\)

⟨⟨125, ⟨6, 9, 
          3⟩⟩, ⟨225, ⟨5, 12, 
          5⟩⟩, ⟨135, ⟨4, 15, 
          7⟩⟩, ⟨27, ⟨3, 18, 
          9⟩⟩⟩

In Mathematica:

(((5  (x1^2) (x2^3) x3 + 3  x1 (x2^6) (x3^3)))^3)

125 (x1^6) (x2^9) (x3^3) + 225 (x1^5) (x2^12) (x3^5) + 
        135 (x1^4) (x2^15) (x3^7) + 27 (x1^3) (x2^18) (x3^9)

Generate 5-Variate Polys over the Finite Field Modulo 13

Theory["F",
	({{Definition["finite field"]}, {Definition["power products"]}, {Definition["pol"]}})]

Definition[\("D", 
	ℙ = 
        pol[finite–field[13], power–products[5]]\)]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Theory["F"], Definition["D"]⟩]

Generate 5-Variate Polys over the 2 Variate Rational Functions over the Finite Field Modulo 13

Theory["F",
	({{Definition["rational"]}, {Definition["power products"]}, {Definition["pol"]}})]

Definition[\("D", 
	ℙ = 
        pol[
quotient–field[
pol[
Galois–field[
                13], 
power–products[
                2]]], 
power–products[5]]\)]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Theory["F"], Definition["D"]⟩]

Object and Meta-level

Proving and Computing

Here is a typical theorem in Groebner bases theory:

Theorem[\("GB", \ 
      any[F], 
is–Groebner–Basis[
            F]⟺\(∀ \+\(f, g ∈ F\)remainder[S–polynomial[f, g], F]\) = 0\)]

We are / will be able to prove it in a formal system (Theorema) by calling

Prove[   Theorem["GB"],      using -> 
        Theory["Polys"],     by -> 
        PL–natural–deduction]

This theorem is also an algorithm. We can use it, in the same logic frame, by calling

\(Compute[\ \ \ 
is–Groebner–Basis[⟨\ \ \ \ \ ⟨\ \ ⟨\ 
              1, \ ⟨1, 
                0⟩⟩\ \ ⟩, \ \ \ \ \ ⟨\ \ ⟨\ 
              1, \ ⟨1, 
                0⟩⟩\ \ ⟩\ ⟩, \ 
using -> ⟨Theorem["GB"], \ 
            Theory["Polys"]⟩], 
by -> PL–simplifier]\)

Computation will be correct for all representations of polynomials that satisfy the properties used in the correctness proof.

The Role of Coding in Correctness Theorems

For applying GB to geo proving, we have to prove the correctness theorem:

Theorem[\("Correctness", \ 
      any[F], 
is–logical–consequence[𝒞, 
            Code[∀ \+x\((Apply[f, x] = \(0 \[Implies] Apply[g, x] = 
                      0\))\)]]⟺
          GB[⟨f, 
              new–indeterminate . g - 1⟩]\  = {1}\)]

𝒞 ... theory of complex numbers  (a bunch of formulae) in some coding.

\(\(Code[∀ \+x\((f \((x)\) = \(0 => g \((x)\) = 
                  0\))\)]\ \  ... \)\ \ a\ coding\ of\ the\ formula\ ' \(∀ \+x\(\(\((f \((x)\) = \(0 => g \((x)\) = 
                  0\))\)'\)\(.\)\)\)\)

For proving this, notions of logic have to be formalized within logic.

Applying Correct Proving Methods

Now, let's assume we managed to prove such a correctness theorem within (an automated version of) predicate logic. (With the progress made in the past years, this seems to be possible.)

Now, we want to apply it:

Formula["1", 
(Underscript[∀ , x, y])((x (y^2) - 
                    x + 1 = 0) ∧ ( 
                (y^2) - x y = 0) \[Implies] ((x^3) y - (x^2) + x = 
                0))]

Prove[ Formula[1],  
      using -> ⟨⟩,   by  -> 
        GB–method]

Now,

(Underscript[∀ , x, y])((x (y^2) - x + 1 = 0) ∧ ( 
              (y^2) - x y = 0) \[Implies] ((x^3) y - (x^2) + x = 
              0))

is a formula of predicate logic. Implicitly, the "universe of discourse" is ℂ.

The GB method, now, is a "built-in" inference rule whose correctness has been proved above.

The inference rule must be "built in" by programming the function GB and auxiliary functions

that have been described / programmed, above, within predicate logic

in the meta-language in which the predicate logic prover is written.

Lifting from the Object Level to the Meta Level

This "lifting" is essential and unavoidable.

This "lifting" is not a special necessity in applying algebraic algorithms to geo proving, but is tacitly ubiquitous in practical proving.

Example:   The proved knowledge

limit[f, a] ∧ limit[g, b]  \[Implies]  
      limit[f + g, a + b]

is lifted to the simplification (inference) rule

(lim_(n -> ∞)) (S + 
            T)    ->    (lim_(n -> ∞)) (S) + (lim_(n -> ∞)) (T)

where S and T are terms and 'lim' is a new quantifier.

The Challenge of Automated Lifting

Without this kind of tacit lifting, practical mathematics would not be possible.  (Practical mathematics is, tacitly, highly structured!)

I think we will need a "lifting operator" that automates lifting in future theorem proving systems.

Conclusion

The computer-supported generation of proofs for automated provers is a challenging task.

Much progress has been made in the past couple of years. 
Highly automated proofs in attractive form seem to be possible "soon".
Still, a lot of work has to be done.

The issue is not so much the one-time verification of correctness theorems which we already know
and not the invention of surprising theorems which we do not yet know
but the possibility to experiment easily with variations of the known theories and theorems.

The lifting of proved knowledge to the level of inference rules is a particularly interesting, challenging, and essential operation for future automated theorem proving systems.