Example of Automated Algorithm Invention 
in Theorema

bruno.buchberger@jku.at
ÖMG Conference, September 25, 2003, Bolzano

Knowledge Base for the Sorting Problem

Definitions

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

({{is–sorted[⟨⟩] }, {(Underscript[∀ , x]) 
                is–sorted[⟨x⟩]}, {\(∀ \+\(x, y, \(z\&-\)\)\)(\(is–sorted[⟨x, y, 
                      z\&_⟩]\)   ⇔{({{x ≥ y}, {\(is–sorted[⟨y, 
                              z\&_⟩]\)}})    })}})

({{⟨⟩≈⟨⟩ }, {\(∀ \+\(y, y\&_\)⟨⟩ ≉ ⟨y, y\&_⟩\)}, {\(\(∀ \+\(x, x\&_, y\&_\)\((⟨x, 
                    x\&_⟩ ≈ ⟨y\&_⟩\  ⇔ \((x ∈ ⟨y\&_⟩ ∧ ⟨x\&_⟩ ≈ 
                      dfo[x, \ ⟨y\&_⟩])\))\)\)\(
\)
          \)}})

({{(Underscript[∀ , x]) 
                x ∉ ⟨⟩}, {\(∀ \+\(x, y, y\&_\)\((x ∈ ⟨y, 
                      y\&_⟩)\)\ \  ⇔ \((\((x = y)\) ∨ 
                    x ∈ ⟨y\&_⟩)\)\)}})

({{(Underscript[∀ , a]) dfo[
                  a,  ⟨⟩] = ⟨⟩}, {\(∀ \+\(a, x, x\&_\)dfo[
                  a, \ ⟨x, x\&_⟩\ ]\) ={({{\(⟨x\&_⟩\), ⇐, x = a}, {\(x⌣
                        dfo[a, \ ⟨x\&_⟩]\), ⇐, otherwise}})} }})

({{\(∀ \+\(y\&_\)\(¬ ⟨⟩ ≻ ⟨y\&_⟩\)\)}, {\(∀ \+\(x, x\&_\)⟨x, 
                  x\&_⟩ ≻ ⟨⟩\)}, {\(∀ \+\(x, x\&_, y, y\&_\)⟨x, 
                    x\&_⟩ ≻ ⟨y, 
                    y\&_⟩\  ⇔ ⟨x\&_⟩ ≻ ⟨y\&_⟩\)}})

\(∀ \+\(x, y\&_\)\((x⌣⟨y\&_⟩ = ⟨x, 
            y\&_⟩)\)\)

\(\(\(∀ \+\(x, y\&_\)\((⟨y\&_⟩⌢x = ⟨y\&_, 
            x⟩)\)\)\(
\)
    \)\)

\(∀ \+X\((is–tuple[
            X]\  ⇔ \ \(∃ \+\(x\&_\)\((X = ⟨x\&_⟩)\)\))\)\)
({{(Underscript[∀ , X])(is–empty–tuple[
                  X]  ⇔ (X = ⟨⟩))}, {(Underscript[∀ , X])(is–singleton–tuple[
                  X]  ⇔ (Underscript[∃ , x])(X = ⟨x⟩))}, {(Underscript[∀ , X])(is–trivial–tuple[
                  X] ⇔ (is–empty–tuple[
                      X] ∨ is–singleton–tuple[X]))}})

Axioms

({{\(∀ \+\(x, x\&_, y, y\&_\)\((⟨x, 
                    x\&_⟩\  = ⟨y, 
                    y\&_⟩)\) ⇔ \((\((x = 
                      y)\) ∧ \((⟨x\&_⟩ = ⟨y\&_⟩)\))\)\)}, {\(∀ \+\(x, x\&_\)⟨x, 
                x\&_⟩ ≠ ⟨⟩\)}})

Properties

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

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y))

({{(Underscript[∀ , is–tuple[X]])X ≈ X}, {(Underscript[∀ , is–tuple[X, Y]])(X ≈ 
                  Y \[Implies] Y ≈ X)}, {(Underscript[∀ , is–tuple[X, Y, Z]])((X ≈ 
                      Y ∧ Y ≈ Z) \[Implies] 
                X ≈ Z)

          }})

({{(Underscript[∀ , is–tuple[X, Y]])(X ≻ 
                  Y \[Implies] (Y ⊁ X))}, {(Underscript[∀ , is–tuple[X, Y, Z]])((X ≻ 
                      Y ∧ Y ≻ Z) \[Implies] 
                X ≻ Z)}})

The Call of the Algorithm Invention Algorithm

Prove[Theorem["correctness of sorting"],  
      using -> Theory["specification of sorting"],  
      by -> 
        Cascade[Induction–Prover,  
          Conjecture–Generator]

The Theorem Automatically Invented by the Method ("Correctness of Merge-Sort Algorithm Schemme")

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

            }, {(Underscript[((Underscript[∀ , is–tuple[
                        X]])), ¬ is–trivial–tuple[X]]){({{left–split[X] ≺ X}, {is–tuple[left–split[X]]}, {right–split[X] ≺ X}, {is–tuple[right–split[X]]}})
}}, {(Underscript[∀ , is–tuple[Y, Z]])is–tuple[
                merged[Y, Z]]}, {(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                        Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})}})}

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

Inventing the Algorithm by Lazy Thinking: First Round

Proof Attempt (Automatically Generated)

For proving the correctness theorem, we use well-founded induction w.r.t. ≻ on X:

We assume

\(is–tuple[⟨xo\&_⟩]\)

and the induction hypothesis

\(\(∀ \+\(is–tuple[Y]\)\)\+\(⟨xo\&_⟩ ≻ Y\)is–sorted–version[Y, 
        sorted[Y]]\)

and we show

\(\(\(is–sorted–version[⟨xo\&_⟩, 
        sorted[⟨xo\&_⟩]]\)\(.\)\)\)

We use the algorithm scheme for 'sorted' and distinguish two cases:

CASE

\(\(\(is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, we have to show

\(is–sorted–version[⟨xo\&_⟩, 
      special[⟨xo\&_⟩]]\)

i.e., by the definition of 'is–sorted–version', we have to show

\(\(\(\((G1)\)\ \ \ \ \ \ is–tuple[
        special[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((G2)\)\ \ \ \ \ \ special[⟨xo\&_⟩] ≈ ⟨xo\&_⟩\)\(,\)\)\)

\(\((G2)\)\ \ \ \ \ \ \(\(is–sorted[
          special[⟨xo\&_⟩]]\)\(.\)\)\)

(G1) is true because of the type requirement for 'special'.

For (G2), by the fact that

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y)),

it suffices to prove that

\(special[⟨xo\&_⟩] = \(\(⟨xo\&_⟩\)\(.\)\)\)

Here we are stuck.

Requirement Automatically Generated

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
          X)

Inventing the Algorithm by Lazy Thinking: Second Round

Proof Attempt

For proving the correctness theorem, we use well-founded induction w.r.t. ≻ on X:

We assume

\(is–tuple[⟨xo\&_⟩]\)

.... exactly as in the first proof attempt ...

We us the algorithm scheme for 'sorted' and distinguish two cases:

CASE

\(\(\(is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, by we have to show

\(is–sorted–version[⟨xo\&_⟩, 
      special[⟨xo\&_⟩]]\)

i.e., because of the definition of 'is–sorted–version', we have to show

\(\(\(\((G1)\)\ \ \ \ \ \ is–tuple[
        special[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((G2)\)\ \ \ \ \ \ special[⟨xo\&_⟩] ≈ ⟨xo\&_⟩\)\(,\)\)\)

\(\((G2)\)\ \ \ \ \ \ \(\(is–sorted[
          special[⟨xo\&_⟩]]\)\(.\)\)\)

(G1) is true because of the type requirement for 'special'.  (G2) is true because of

(Underscript[∀ , is–trivial–tuple[X],  is–tuple[Y]])(X ≈ 
            Y ⇔ (X = Y)),

and the new requirement

(Underscript[∀ , is–trivia–tuple[X]])(special[X] = 
            X).

(G3) is true because of the same requirement and the following property of 'sorted'

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

CASE

\(\(\(¬ is–trivial–tuple[⟨xo\&_⟩]\)\(:\)\)\)

In this case, we have to show

\(\(\(is–sorted–version[⟨xo\&_⟩, 
        merged[sorted[
            left–split[⟨xo\&_⟩], 
            sorted[right–split[⟨xo\&_⟩]]]]]\)\(.\)\)\)

For this, by the definition of 'is–sorted–version', it suffices to show

\(\(\(\((H1)\)\ \ \ \ \ \ is–tuple[
        merged[sorted[
            left–split[⟨xo\&_⟩], 
            sorted[right–split[⟨xo\&_⟩]]]]]\)\(,\)\)\)

\(\(\(\((H2)\)\ \ \ \ \ ⟨xo\&_⟩ ≈ 
      merged[sorted[
          left–split[⟨xo\&_⟩], 
          sorted[right–split[⟨xo\&_⟩]]]]\)\(,\)\)\)

\(\((H3)\)\ \ \ \ \ \(\(is–sorted[
          merged[sorted[
              left–split[⟨xo\&_⟩], 
              sorted[right–split[⟨xo\&_⟩]]]]]\)\(.\)\)\)

>From the case assumption, by the type requirements on 'left–split' and 'right–split', the property that 'left–split' and 'right–split' produce shorter tuples, and the induction hypothesis we obtain

\(\(\(is–sorted–version[
      left–split[⟨xo\&_⟩], 
      sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(is–sorted–version[
        right–split[⟨xo\&_⟩], 
        sorted[right–split[⟨xo\&_⟩]]]\)\(.\)\)\)

>From this, by the definition of 'is–sorted–version', we obtain

\(\(\(\((AL1)\)\ \ \ \ \ is–tuple[
        sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AL2)\)\ \ \ \ \ left–split[⟨xo\&_⟩] ≈ 
      sorted[left–split[⟨xo\&_⟩]]\)\(,\)\)\)

\(\(\(\((AL3)\)\ \ \ \ \ is–sorted[
        sorted[left–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AR1)\)\ \ \ \ \ is–tuple[
        sorted[right–split[⟨xo\&_⟩]]]\)\(,\)\)\)

\(\(\(\((AR2)\)\ \ \ \ \ right–split[⟨xo\&_⟩] ≈ 
      sorted[right–split[⟨xo\&_⟩]]\)\(,\)\)\)

\(\((AR3)\)\ \ \ \ \ \(\(is–sorted[
          sorted[right–split[⟨xo\&_⟩]]]\)\(.\)\)\)

(H1) follows from (AL1) and (AR1) by the type requirement on 'merged'.

Now we are stuck.

Requirement Automatically Generated

(Underscript[((Underscript[∀ , is–tuple[X, Y, 
                Z]])), ¬ is–trivial–tuple[X]])({({{left–split[X] ≈ Y}, {right–split[X] ≈ Z}, {is–sorted[Y]}, {is–sorted[Z]}})}\[Implies]{({{merged[Y, Z] ≈ X}, {is–sorted[merged[Y, Z]]}})})

Inventing the Algorithm by Lazy Thinking: Last Round

We now do exactly the same proof attempt once more.

This time, the inductive proof will succeed using the added requirement on  'left-split', 'right-split' und 'merged' for proving (H2) and (H3).

If we now collect the requirements on the functions'special','left-split','right-split',and'merged', we obtain the "Correctness Theorem for Merge-Sort" formulated at the beginning of this paper.