TH∃OREM∀
A Short Demo

Bruno Buchberger, C. Dupre', T. Jebelean, K. Kriftner
K. Nakagawa, D. Vasaru,  W. Windsteiger

Research Institute for Symbolic Computation
Johannes Kepler University, A4040 Linz, Austria
                Theorema@Theorema.org

Copyright Bruno Buchberger and Theorema Working Group 1999: Copying, storing in data bases etc. is granted under the condition that the file is kept unchanged and this copyright note is included in the copy. Usage of the material contained in this talk has be cited appropriately.

Version: 2000-1-22

Acknowledgements: This research is partially supported by the Austrian Science Foundation (FWF-SFB-project FO-1302) and the Upper Austrian Government  (project ``PROVE'').

The Purpose of this Demo

The Theorema system is a system for proving, solving, and simplifying mathematical formulae. It is programmed in the Mathematica language, version 3.0 or later, and also heavily uses the front-end of Mathematica. Theorema can therefore be used on all machines on which Mathematica, version 3.0 or later, is installed.

Theorema is being developed by the TH∃OREM∀ Working Group at the RISC institute under the direction of Bruno Buchberger. The current members of the TH∃OREM∀ Working Group are B. Buchberger, C. Dupre, F.Kriftner, T. Jebelean, K. Nakagawa, D. Vasaru, and W.Windsteiger.

The Theorema demo presented in this notebook demonstrates the most important functionalities of  Theorema Version 1.0 (1999). I used this demo 1999 in a couple of talks on Theorema at various occasions. The varying parts of these talks, emphasizing various different aspects of the system,  are contained in extra files (which will soon be available over the web) and refer to this file for the demo part.

This file can be read if you have Mathematica installed on your machine. If not, you can read the postscript version Theorema-Demo-1999.ps of this file.

If you are an alpha tester of Theorema you can execute and play with the commands given in this file. Currently, we do not accept any more alpha testers. The beta version of Theorema will most probably be released in Fall 2000. If you want to be informed about the release, i.e. if you want to become a beta tester, please, write to Theorema@Theorema.org.

Example: Greatest Common Divisor

Start Theorema

The following command loads the basic Theorema files.

Needs["Theorema`"]

The subsequent commands load a version of Theorema's predicate logic prover and initializes certain options. All this is necessary for running the example in this section.

InitializeGlobals[
        Evaluator -> EvaluateFromInnermost];

Use[
      ⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], 
        Built–in["Numbers"]⟩]

\(SetGlobals[TraceLevel -> 0, SearchDepth -> 100, 
      DebugLevel -> 0]; $RecursionLimit = 1024; 
    Needs["Theorema`Provers`UserProvers`PCS`"]; \ Off[General::spell]; 
    Off[General::spell1]; $TmaQRTarget = {"kb", "goal"}; $TmaProofPresentation = "SuccessBranch";\)

The Purpose of this Example

This examples shows how, in Theorema, the entire cycle of "doing mathematics", i.e.

defining a new notion

formulating conjectures about the notion

proving the conjectures

using proved theorems as "methods" ("algorithms") for particular inputs

can be fully supported.

In particular, we emphasize the unique feature of Theorema that, without leaving the system, mathematical formulae can be both viewed as statements (e.g. definitions or theorems that need to be proved) and also as algorithms (that can be executed on particular inputs, in case the statements are "algorithmic").

Definition

Here, is a definition of the notion "greatest common divisor", which can be made known to Theorema by typing it into an input cell:

Definition[\("greatest common divisor", any[m, n], 
      
	gcd[m, n] = 
        \(\(max\+\(d = 1, …, m\)\)\+\(\((d ∣ m)\) 
                ∧ \((d ∣ n)\)\)\) d\)]

This formula can be viewed as a logical statement that is true for all m, n (in the universe of natural numbers, which we do not specify explicitly here, i.e. we consider the domain of natural numbers as the "universe of discourse"). However, it can also be viewed as a statement that describes how, for arbitrary m, n, gcd[m,n] can be computed. If we want to use this formula in this way for computing, say, gcd[24,32] we enter:

Compute[gcd[24, 32], 
      using -> Definition["greatest common divisor"]]

Note that by setting the option 'using' to 'Definition["greatest common divisor"]' the system is told to use, as its only knowledge - except some built-in knowledge about the maximum quantifier and the like - the above definition. (Built-in knowledge can be specified by the 'Use' command, see the subsubsection on Starting Theorema above).

Here are some other calls of 'gcd' together with their timings:

Compute[gcd[24, 32], 
        using -> Definition["greatest common divisor"]] // Timing

Compute[gcd[240, 320], 
        using -> Definition["greatest common divisor"]] // Timing

Compute[gcd[2400, 3200], 
        using -> Definition["greatest common divisor"]] // Timing

Compute[gcd[24000, 32000], 
        using -> Definition["greatest common divisor"]] // Timing

As expected, the computing time roughly grows linearly. (The absolute timings are quite high. This is so because the formulae are "interpreted" not "compiled". In this version, Theorema is a research and teaching tool and not a tool to be used for serious computations. A later version of Theorema will make the execution of formulae much faster.)

Euclid's Theorem

Now, somebody like Euclid (300 B.C) may come up with the following, nontrivial, conjecture about the notion '∣' ('divides'):

Proposition[\("divides difference", any[d, m, n], 

      	\((d ∣ m ∧ d ∣ n)\)\ \ \ \ \ \ \ \ \ 
        ⟹\ \ \ \ \ \ \ \((d ∣ m - n)\)\)]

from which the following variant

Proposition[\("common divisors and difference", 
      any[d, m, n], 
	
      \((d ∣ m ∧ d ∣ n)\)\ \ \ \ \ \ \ \ \ 
        ⟺\ \ \ \ \ \ \ 
        \((d ∣ m - n\ \ \  ∧ \ \ \ \ d ∣ n)
          \)\)]

and also the following theorem on 'gcd'

Proposition[\("Euclid's Theorem", any[d, m, n], 
	
      gcd[m, n] = 
        \[LeftDoubleBracketingBar]gcd[m - n, n] ⇐ m > n, 

          			\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 
          gcd[m, n - m] ⇐ n > m, 

          			\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ m
          \[RightDoubleBracketingBar]\)]

easily follow. (In Theorema, the symbol '‖...‖' is used for the case statement.)

The benefit we get from the mathematical knowledge described in this proposition is enormous:

Compute[gcd[24, 32], 
        using -> Proposition["Euclid's Theorem"]] // Timing

Compute[gcd[240, 320], 
        using -> Proposition["Euclid's Theorem"]] // Timing

Compute[gcd[2400, 3200], 
        using -> Proposition["Euclid's Theorem"]] // Timing

Compute[gcd[24000, 32000], 
        using -> Proposition["Euclid's Theorem"]] // Timing

We see that, for drastically increasing input, the computing time only increases mildly.

This examples shows the essence of mathematics and the value of mathematical knowledge: Spend your time for thinking once about why a certain knowledge is true (i.e. spend your time once for proving), then you can save time infinitely many times.

Now the question is: Can we automate proving?

An Automated Proof of Euclid's Theorem

We now demonstrate, how Theorema can be used not only for computing but also for proving. We show this in the example of the essential proposition on which Euclid's Theorem is based:

Proposition["divides difference",any[d, m, n],
	({{(d ∣ m ∧ 
                    d ∣ 
                      n)         ⟹       (d ∣ m - n    ∧     d ∣ n), "divdiff"}})]

Of course, in order to prove this, we need the definition of '∣':

Definition["divides",any[d, m],
	({{(d ∣ m)            
                ⟺          
                (Underscript[∃ , f])((d f) = m), "div:"}})]

and also the fundamental knowledge about the interplay of multiplication and subtraction:

Proposition["distributivity",any[d, u, v, m, n],
	({{((d u = m) ∧ (d v = 
                        n))            ⟹         ( d (u - v) = m - n), "distr"}})]

Now, for proving the proposition, all we have to do in Theorema is to call one of the Theorema provers (whose name is "PC" for "prove by applying Proof and Computation steps", which is a new prover for predicate logic formulae developed by the author):

\(Prove[
      Proposition["divides difference"], 
	\ using -> ⟨Definition["divides"], 
          Proposition["distributivity"]⟩, 
	\ by -> PC]\)

i.e. we just have to tell the system

the proof goal 'Proposition["divides difference"]',

the knowledge base  'Definition["divides"]' and 'Proposition["distributivity"]' which we allow the prover to use in the proof,

and the particular prover 'PC' we want to try on this proof problem.

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers, we have stored this notebook  under the name Theorema-Demo- 1999-Proof-GDC.nb or, alternatively, the name Theorema-Demo-1999-Proof-Proof-GDC.ps.) Note that every single (English) word and every formula in this proof is generated automatically by the Theorema prover 'PC' (i.e. without any further help and interaction by the user). Also, we hope you will appreciate that the proof text is very natural and resembles the style a (good) mathematician would present the proof.  If you don't want to see all the details of the proof, you can use the nested cell brackets at the right-hand margin for "closing" (making invisible) certain parts of the proof. Of course, the closed parts are still there, they just are not shown any more. You can re-open closed cells by clicking again into the respective bracket.

Example: Analysis

The Purpose of this Example

This examples shows how, in Theorema, a typical portion of mathematical text can be formalized and the respective proofs can be generated automatically.

It is interesting to note in this example that, in contrast to wide-spread but wrong opinion, formal proving does not mean "proving from first principles", that formal proving does not necessarily imply that the proofs generated are long or "hard to read", and that amazingly small knowledge bases suffice for the proof of interesting theorems in advanced areas of mathematics. This is not amazing for people who understand that good mathematics is well structured in "layers" of knowledge about the various mathematical notions in the same way as good software is well structured in layers of  algorithms (modules).

Clear

In this section we do not want to use any "built-in" knowledge. For this, we just say

Use[{}]

Limit of Sum: Preliminaries

We show the example of a proof in elementary analysis. Here is the usual definition of the predicate 'limit[f,a]' ('a is the limit of the sequence f'):

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

We want to prove the following theorem:

Proposition["2-ary limit of sum",any[f, a, g, b],
	
	({{(limit[f, a] ∧ limit[g, b])
                  ⟹limit[f + g, a + b],        "l2+"}})]

In fact, with a stronger version of the prover 'PC', namely 'PCS' (see next section), we can produce a proof of this theorem completely automatically. However, here, we want to demonstrate how the proof can be built up in several "layers" that correspond to the layers naturally suggested by the "alternating quantifiers" in the definition of the limit notion. For this, we decompose the definition into several auxiliary definitions so that in each definition only one quantifier is introduced:

Definition["4-ary limit",
	({{(Underscript[∀ , f, a, ϵ, N
                  ])limit[f, a, ϵ, N]
                    ⟺(Underscript[((Underscript[∀ , n])), n 
                        ≥ N
                        ])\[LeftBracketingBar]f[n] - a\[RightBracketingBar] < 
                      ϵ, "l4:"}})]

Definition["3-ary limit",
	({{(Underscript[∀ , f, a, 
                  ϵ])limit[f, a, ϵ]
                    ⟺(Underscript[∃ , N]) limit[f, a, 
                      ϵ, N], "l3:"}})]

Definition["2-ary limit",
	({{(Underscript[∀ , f, a
                  ])limit[f, a]
                    ⟺(Underscript[((Underscript[∀ 
                          , ϵ])), ϵ > 0])limit[f, a, 
                      ϵ], "l2:"}})]

Note that, in these definitions, "4-ary limit", "l4:" etc. are labels. They do not add to the logical meaning of the formulae but are introduced only for being able to refer easily to these formulae in proofs etc.

Making these layers in the definition explicit will not only help the 'PC' prover to find the proof without user interaction but we found, in teaching experiments with students, that breaking down such definitions according to the quantifier structure also helps in understanding notions introduced by alternating quantifiers. (Please, think about the intuitive and graphical meaning of each of these notions. For example, 'limit[f,a,ϵ,N]' means that the sequence f stays closer to the value a than ϵ from index N on.)

Correspondingly, we also break down the proposition into three layers. Each of these propositions describes the effect of addition on sequences for the corresponding layer of the limit notion:

Proposition["4-ary limit of sum",any[f, a, δ, M, g, b, ϵ, N],
	({{\(\((limit[f, a, δ, M] ∧ 
                    limit[g, b, ϵ, N])\) \[Implies] 
	
                limit[f + g, a + b, δ + ϵ, max[M, N]]\), "lim+"}})]

Proposition["3-ary limit of sum",
	({{\(∀ \+\(f, a, δ, g, b, ϵ\)\((
                  \((limit[f, a, δ] ∧ limit[g, b, ϵ])\)

                    	⟹limit[f + g, a + b, 
                      δ + ϵ])\)\), "l3+"}})]

Proposition["2-ary limit of sum",any[f, a, g, b],
	
	({{(limit[f, a] ∧ limit[g, b])
                  ⟹limit[f + g, a + b],   
              "l2+"}})]

Proof of the Proposition on the 4-ary Limit

For proving Proposition["4-ary limit of sum"], in addition to Definition["4-ary limit"], the following knowledge is sufficient:

Definition["sum of sequences",any[f, g, x],
	({{(f + g)[x] = f[x] + g[x], "+:"}})]

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

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

We collect this knowledge in one little "theory" by entering the following Theorema instruction:

Theory["4-ary limit",
	({{Definition["4-ary limit"]}, {Definition["sum of sequences"]}, {Lemma["distance of sum"]}, {Lemma["maximum"]}})]

Now the proof of Proposition["4-ary limit of sum"] can be generated, fully automatically, by the following Theorema call:

Prove[Proposition["4-ary limit of sum"], 
      using -> Theory["4-ary limit"], by -> PC]

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers, we have stored this notebook under the name Theorema-Demo-1999- Proof-4-ary-Limit.nb or, alternatively, the name Theorema-Demo-1999-Proof-4-ary-Limit.ps.)

Proof of the Proposition on the 3-ary Limit

For proving Proposition["3-ary limit of sum"], the following knowledge is sufficient:

Theory["3-ary limit",
	({{Proposition["4-ary limit of sum"]}, {Definition["3-ary limit"]}})]

Here is the Theorema call for generating the proof:

Prove[Proposition["3-ary limit of sum"], 
      using -> Theory["3-ary limit"], by -> PC]

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers, we have stored this notebook under the name Theorema-Demo-1999-Proof- 3-ary-Limit.nb or, alternatively, the name Theorema-Demo-1999-Proof-3-ary-Limit.ps.)

Proof of the Proposition on the 2-ary Limit

For proving Proposition["2-ary limit of sum"], the following property is necessary:

Proposition["positiveness",
	({{(Underscript[((Underscript[∀ , a])), a > 0])(a/2) > 0, "/2>"}})]

Also, we need a slight variant of Proposition["3-ary limit of sum"]:

Proposition["3-ary limit of sum: variant",
	({{\(∀ \+\(f, a, g, b, ϵ\)\((
                  \((limit[f, a, ϵ/2] ∧ 
                        limit[g, b, ϵ/2])\)
	
                    ⟹limit[f + g, a + b, ϵ])
                  \)\), "l3+"}})]

which could be proved easily from Proposition["3-ary limit of sum"].

Now, the prerequisite knowledge base for the proof is:

Theory["2-ary limit",
	({{Definition["2-ary limit"]}, {Proposition["3-ary limit of sum: variant"]}, {Proposition["positiveness"]}})]

Here is the Theorema call for generating the proof:

Prove[Proposition["2-ary limit of sum"], 
      using -> Theory["2-ary limit"], by -> PC]

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers, the notebook generated is available under the name Theorema-Demo- 1999-Proof-2-ary-Limit.nb or, alternatively, the name Theorema-Demo-1999-Proof-2-ary-Limit.ps.)

Continuity of Product

Similarly, we could now start to prove theorems about the notion of cotinuity:

Definition["2-ary continuity",any[f, x],
	({{continuous[f, x]
                  ⟺(Underscript[((Underscript[∀ 
                        , ϵ])), ϵ > 0])continuous[f, x, 
                    ϵ], "c2:"}})]

Definition["3-ary continuity",any[f, x, ϵ],
	({{continuous[f, x, ϵ]
                  ⟺(Underscript[((Underscript[∃ 
                        , δ])), δ > 0])continuous[f, x, 
                    ϵ, δ], "c3:"}})]

Definition["4-ary continuity",any[f, x, ϵ, δ],
	({{continuous[f, x, ϵ, δ]
                  ⟺(Underscript[((Underscript[∀ , y])
                        ), \[LeftBracketingBar]x - y
                          \[RightBracketingBar] < 
                      δ])\[LeftBracketingBar]f[x] - 
                        f[y]\[RightBracketingBar] < ϵ, "c4:"}})]

Proposition["4-ary continuity of product",any[f1, x, ϵ1, δ1, 
          f2, ϵ2, δ2],
	({{\(\((continuous[f1, x, ϵ1, δ1] ∧ 
                    continuous[f2, 
                      x, ϵ2, δ2])\) \[Implies] 
	
                continuous[f1*f2, 
                  x, ϵ1*\((ϵ2 + \[LeftBracketingBar]f2[
                              x]\[RightBracketingBar])\) + \[LeftBracketingBar]f1[x]\[RightBracketingBar]*ϵ2, 
                  min[δ1, δ2]]\), "cont[ * ]"}})]

Definition["product of functions",any[f, g, x],
	({{(f*g)[x] = f[x]*g[x], "f*g"}})]

Lemma["distance of product",any[a1, a2, b1, b2, δ1, δ2],
	({{\(\((\[LeftBracketingBar]\((b1*b2)\) - 
                        \((a1*a2)\)\[RightBracketingBar] < 
                    \((δ1*
                          \((δ2 + 
                              \[LeftBracketingBar]b2\[RightBracketingBar])
                            \) + \[LeftBracketingBar]b1\[RightBracketingBar]*
                          δ2)\))\)⟸
	
                \((\[LeftBracketingBar]b1 - a1\[RightBracketingBar] < 
                      δ1 ∧ 
                    \[LeftBracketingBar]b2 - a2\[RightBracketingBar] < 
                      δ2)\)\), "| * |"}})]

Lemma["minimum",any[m, M1, M2],
({{m < min[M1, M2] \[Implies] (m < M1 ∧ m < M2), "min<"}})]

Theory["4-ary continuity of product",
	({{Definition["4-ary continuity"]}, {Definition["product of functions"]}, {Lemma["distance of product"]}, {Lemma["minimum"]}})]

\(Prove[Proposition["4-ary continuity of product"], 
      using -> Theory["4-ary continuity of product"], 
	
      by -> PC]\)

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers, we stored this notebook under the name Theorema-Demo- 1999-Proof-4-ary-Continuity.nb or, alternatively, the name Theorema-Demo-1999-Proof-2-ary-Continuity.ps.)

We hope that now it should be clear how the proof of the 3-ary and 2-ary variants of the continuity proof could be generated in Theorema.

Example: Predicate Logic Proving by "Prove - Compute - Solve"

The Purpose of this Example

This examples shows how, in Theorema, with a much more powerful prover, which we call the "PCS-prover" ("Prove, Compute, Solve"), the proof of the above theorems and similar theorems can be generated completely automatically without inventing the intermediate 3-ary and 4-ary variants of the theorems. The PCS-method has been proposed recently by the author and is currently one of the main research topics within the Theorema project.

The essential new ingredient into the PCS-prover is a method by which a proof problem, after the PC-phase, is converted into the problem of  "finding" appropriate values that make certain formulae true under the assumptions in the current knowledge base and this problem is then solved by calling a solver (like, for example, Collins' method) for formulae of the theory of real closed fields or another appropriate solver depending on the type of the variables involved.

Limit of Sum: Preliminaries

With the PCS-prover, for the proof of Proposition["2-ary limit of sum"], it suffices to provide the following knowledge base:

Theory["2-ary limit",
	({{Definition["2-ary limit"]}, {Definition["sum of sequences"]}, {Lemma["distance of sum"]}, {Lemma["maximum"]}})]

Limit of Sum: Proof

With the PCS-prover, the  automatic generation of the proof does not need any more user interaction. In particular, it does not need the invention of the intermediate lemmata for the 4-ary and 3-ary versions of the limit notion:

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

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you have the latest, January 2000, version of Theorema available you can execute the above command and actually generate this notebook. For the other readers we stored this notebook  under the name Theorema-Demo-1999-Proof-2-ary-Limit-with-PCS.nb or, alternatively, the name Theorema-Demo- 1999-Proof-2-ary-Limit-with-PCS.ps.)

Example: Set Theory Proving

Load Prover

For generating proofs involving set theory notions, we have to load the Theorema set theory prover:

Needs["Theorema`Provers`UserProvers`SetTheoryProver`"]

MakeBoxes[Floor[a_], StandardForm] := 
      RowBox[{"⌊", MakeBoxes[a, StandardForm], 
          "⌋"}]

The Purpose of this Example

This examples shows how, in Theorema, with an extension of the PCS-prover for predicate logic, proofs for theorems involving notions of set theory can be generated. The style of the proofs generated is very much the same as the style of the proofs generated by the predicate logic prover (PC or PCS). The basic properties of the set theoretic notions (like the extensionality axiom for equality between sets) are not added to the knowledge base but, rather, are incorporated as additional inference rules.

The example also shows, how playing with Theorema can reveal the exact dependence of certain theorems on a minimal knowledge base. For example, the proof of  Proposition["Classes Modulo Symmetric Predicates"] in the next section needs only the symmetry of the relation ~ considered and does not need reflexivity nor transitivity.

Classes Modulo Relations

We demonstrate the set theory prover (which currently, January 2000, is only in its initial state of development) by an easy example proof of a statement on residue classes. We start with the definition of the notion of a symmetric relation:

Definition["Symmetry",any[ ∼ ],
	({{is–symmetric[ ∼ ] ⇔ (Underscript[∀ , a, b])(a ∼ b \[Implies] b ∼ a), "symm:"}})]

Note that, in this definition, "~" is a variable (in fact, a higher-order variable) for arbitrary binary predicates.

Now we define the residue class of a modulo ~:

Definition["Classes Modulo a Predicate",any[ ∼ , a],
	({{⌊a⌋_ ∼    = {
                  b  (Underscript[\[VerticalSeparator], b])(b ∼ a)}, "⌊ ⌋:"}})]

We now prove the following proposition:

Proposition["Classes Modulo Symmetric Predicates",any[ ∼ ],
	({{is–symmetric[ ∼ ] \[Implies] (Underscript[∀ , a, b])(a ∈ ⌊b⌋_ ∼  \[Implies] 
                      b ∈ ⌊a⌋_ ∼ ), "symm\[Implies]⌊⌋"}})]

Here is the proof call in Theorema:

\(Prove[Proposition["Classes Modulo Symmetric Predicates"], 
	
      using -> 
        ⟨Definition["Symmetry"], 
          Definition["Classes Modulo a Predicate"]⟩, 

      	by -> SetTheoryPCProver, 
      presentation -> "SuccessBranch"]\)

The option 'presentation->"SuccessBranch"' is chosen for suppressing, in the output, all intermediate proof attempts so that only the successful attempt is finally shown.

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you have the latest, January 2000, version of Theorema available you can execute the above command and actually generate this notebook. For the other readers we stored this notebook under the name Theorema-Demo-1999-Proof-Symmetric-Relations.nb or, alternatively, the name Theorema-Demo-1999- Proof-Symmetric-Relations.ps.)

Example: Inventing Lemmata on Natural Numbers

Load Induction Provers

Now we load an induction prover for proving equalities on natural numbers:

\(\(\( (*\ \(Needs["Theorema`Language`Semantics`UserLanguage`"];\)*) \)\(SetGlobals[LabelStyle -> "Numeric", 
      Prover -> NNEqIndProver]; 
    Needs["Theorema`Provers`Cascade`Cascade`"]; 
    Needs["Theorema`Provers`Cascade`ConjectureGenerator`"]\)\)\)

The Purpose of this Example

In this section, we do not only demonstrate how a typical Theorema induction prover works but, more importantly how any prover P, for example the induction prover for equalities over natural numbers, can be combined with a "conjecture generator" C in a process which we call "cascade" for obtaining a new prover  which, often, is much more powerful than the original prover and, in addition, during the process of generating proofs, invents and adds useful new knowledge to the knowledge base without any user interaction.

What the meta-algorithm Cascade[P,C] (that depends on the prover P and the conjecture generator C) does  is, roughly, the following:

For proving a goal G relative to a knowledge base K, it attempts to generate a proof by using P.

If the attempt is successful, we are done, and the proof is output.

If the attempt fails, C analyzes the failing proof and produces, from the line in which the proof fails, a conjecture ("lemma") L.

Now, Cascade[P,C] is called recursively for attempting to generate a proof for L relative to the knowledge base K. (Note that this recursive call may produce and prove more conjectures than just L!)

If this call succeeds, i.e. L can be proved, Cascade[P,C] is called recursively for the goal G but, now, relative to the new knowledge base K augmented by L and all proved lemmata that have been produced during the proof of L.

If this call fails, the cascade stops unsuccessful. (Note, however, that even in the unsuccessful case a couple of lemmata may have been proved!)

Inductive Definition of Addition

We show the effect of the cascade in the case of proving, by induction, commutativity for addition on the natural numbers:

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

A Failing Proof

We now try to prove commutativity of addition with one of the Theorema induction provers (whose name is 'NNEqIndProver') for natural numbers:

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

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

(SuperPlus[(Subscript[m, 1])])=(SuperPlus[(0+(Subscript[m, 1]))])

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. Otherwise, please, open the file Theorema-Demo-1999-Proof-Attempt-Commutativity.nb or, alternatively, the file Theorema-Demo-1999-Proof-Attempt-Commutativity.ps.)

If you study this proof carefully you will immediately understand how the prover 'NNEqIndProver' works. It turns out that it cannot complete the proof because it would have to "know", for some "arbitrary but fixed"  (Subscript[m, 1]), that

(SuperPlus[(Subscript[m, 1])])=(SuperPlus[(0+(Subscript[m, 1]))])

A human reader would probably immediately conjecture that, maybe, 0 is also a left-zero for addition, i.e.

(Underscript[∀ , m]) m = 0 + m

and that, if this formula was true and was added to the knowledge base, the proof of commutativity could be continued and, maybe, could be completed. (In fact, as we will see this formula is true and the proof of commutativity can be continued but it cannot yet be completed. Rather, the proof will again be stuck at an equality that cannot be proved because, before this, another lemma should have been proved!) All this is now automatically done by the "meta-algorithm" 'Cascade':

Learning from Failure: The 'Cascade'

We now call, instead of just 'NNEqIndProver', the 'Cascade[NNEqIndProver,ConjectureGenerator]', in which 'NNEqIndProver' is combined in the way described above with a 'ConjectureGenerator' that simulates, essentially, the conjecturing strategy of a human:

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

This call generates, without any user-interaction, a sequence of altogether five notebooks containing all intermediate proofs and proof attempts. The names of these notebooks are 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. Otherwise, please, open the files Theorema-Demo-1999-Cascade-1.nb until Theorema-Demo-1999-Cascade-5.nb or, alternatively, the files Theorema-Demo-1999-Cascade-1.ps until Theorema-Demo-1999-Cascade-5.ps.) In order to understand the effect of the cascade it is important to study these notebooks, at least to the extend that you see which goals are proved (are attempted to be proved) with respect to which knowledge bases. The final notebook contains not only a successful proof of commutativity but, in addition, contains two more lemmata in the knowledge base that have been invented (!) and proved in the course of the entire cascade. Also note that, in fact, the lemmata invented by the cascade are "interesting" and "natural" lemmata, namely:

the property that 0 is also a left-zero and

addition also obeys induction from left.

In fact, it is quite natural that these two lemmata should be proved before one attempts to prove commutativity of addition and this is what the cascade detects completely automatically!

Example: Special Proof Rules for Natural Numbers

The Purpose of this Example

In the previous example, we demonstrated how the proving power of a given prover P can be increased drastically by combining it with a "conjecture generator" C in the cascade mode. Here, by "increased proving power" we mean that "more theorems can be proved".

In the next example, we want to demonstrate how the proving power of a given prover P can be increased by incorporating proved knowledge into the prover itself, i.e. by using proved knowledge not as a part of the knowledge base but as a new inference rule. In this approach, by "increased proving power" we mean that "theorems can be proved in fewer steps", i.e. by "leaving out uninteresting steps".

As an example, we use commutativity and associativity of addition on natural numbers:

In the first of the two subsequent sections, we will first prove, by the induction prover 'NNEqIndProver' associativity of multiplication using (among other properties) commutativity and associativity of addition in the knowledge base. This will result in a successful proof that contains, however, long sequences of steps that do nothing else than to apply commutativity and associativity of addition and, at the stage of exploring the theory of multiplication, are not any more "interesting".

In the second of the two subsequent sections, we will prove commutativity of multiplication again by the induction prover 'NNEqIndProver' but in a variant in which iterated associativity of multiplication is used as a "black box simplification step" that brings any term immediately into a "normal form" w.r.t. to associativity and commutativity (AC) of addition. Roughly, this simplification "uniquely orders the terms in a sum and brings all parentheses to their left-most position". This variant of the prover 'NNEqIndProver' produces a proof that replaces every  sequence of "uninteresting" AC-steps by one "AC-simplification" step.

This principle of "elevating knowledge (like the laws of associativity and commutativity) to the level of inference rule (like AC-simplification)" is of utmost importance to making automated proving feasible and, in fact, is a key strategy in human proving. This strategy, so far, is not really systematically studied in the literature and will be one of the key techniques in the Theorema project.

Using Associativity and Commutativity as Part of the Knowledge Base

We start from an exhaustive knowledge base for addition

Propositions["Equational Properties of Addition",any[m, n, p],
	({{m + 0 = m, " +0"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + ^+"}, {0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}, {m + n = n + m, " + "}, {(m + n) + p = m + (n + p), "( + ) + "}})]

and a partial knowledge base for multiplication:

Propositions["Some Equational Properties of Multiplication",any[m, n],
	({{m*0 = 0, " *0"}, {\(m*\(n\^+\) = \((m*n)\) + m\), " *  ^+"}, {0*n = 0, "0*"}, {\(\(m\^+\)*n = \((m*n)\) + n\), " ^+*"}})]

Now, we prove associativity of multiplication using, first, the prover 'NNEqIndProver' in its original form:

Proposition["Associativity of Multiplication",any[m, n, p],
	({{(m*n)*p = m*(n*p), "( * ) * "}})]

Prove[\(Proposition["Associativity of Multiplication"], 
	
      using -> {Propositions["Some Equational Properties of Multiplication"], 
          Propositions["Equational Properties of Addition"]}, \ 
	
      by -> NNEqIndProver, presentation -> "SuccessBranch"\)]

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers we have stored this file under the name Theorema-Demo-1999- Proof-Associativity.nb or, alternatively, the name Theorema-Demo-1999-Proof-Associativity.ps.)

In order to really understand the essence of the strategy, it is important that you study this proof. In particular, analyze the sequences of steps in which associativity and commutativity of addition is used. Two important examples of such sequences are the ones occurring right at the end (in the most important part) of the proof.

Using Associativity and Commutativity as Inference Rules

Now we remove associativity and commutativity of addition from the knowledge base:

Propositions["Equational Properties of Addition",any[m, n, p],
	({{m + 0 = m, " +0"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + ^+"}, {0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}})]

Instead, we call 'NNEqIndProver' in a variant that uses associativity and commutativity of addition for special simplification. This variant can be called by setting the option 'built–in -> {Property[+->  {Associative, Commutative}]}'. (Of course, AC-simplification must be implemented extra in Theorema, it does not "come for free".)

Prove[\(Proposition["Associativity of Multiplication"], 
	
      using -> {Propositions["Some Equational Properties of Multiplication"], 
          Propositions["Equational Properties of Addition"]}, \ 
	
      built–in -> {Property[\(+\(\(->\)\({Associative, 
                  Commutative}\)\)\)]}, 
	by -> NNEqIndProver, 
      proof–object -> "SuccessBranch"\)]

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers we stored the file under the name Theorema-Demo-1999- Proof-Associativity-with-AC.nb or, alternatively, the name Theorema-Demo-1999-Proof- Attempt-Associativity-with-AC.ps.)

Again, we ask you to study the proof carefully in order to see the effect of AC-simplification: The proof is much shorter, it replaces every sequences of AC-steps by a standard AC-simplification step (marked by '(SpecialSimp)') in the proof. Also, if you are a Theorema tester, you will notice that the computing time for the proof is much shorter!

Example: Proving Booleans of Equalities by Groebner Bases

The Purpose of this Example

In the next example, we want to demonstrate how the technique of  using proved knowledge not as a part of the knowledge base but as a new inference rule can be made arbitrarily powerful. Entire mathematical theories can be turned into "black box" inference rules (i.e. into inference rules whose application may involve millions of individual steps that are, however, not shown to the user because their correctness has been proved, once and for all, by the underlying mathematical theory).

One such method is the method of "Groebner bases" invented by the author in his PhD thesis 1965 and published in B. Buchberger, An Algorithmic Criterion for the Solvability of Nonlinear Systems of Algebraic Equations, Aequationes Mathematicae, 4/3, pp. 374-383, (1970). The original version of this paper is in German, an English version is re-printed in B. Buchberger, F. Winkler (eds.), Groebner Bases and Applications, Cambridge University Press, 1998, pp. 535-545. In this book (pp. 3-31), there is also a survey paper on Groebner bases that contains a  detailed but concise version of the proof of the author's main theorem of Groebner bases theory: B. Buchberger, Introduction to Groebner Bases. Proving and disproving arbitrary universally quantified Boolean combinations of equalities over any algebraically closed field can be reduced to the decision about the solvability of systems of nonlinear multivariate polynomials equations. It can be proved, once and for all, that any such decision can be made by checking whether or not the constant 1 is in the corresponding Groebner basis and an algorithm can be established that computes the "corresponding" Groebner basis for any set of nonlinear multivariate polynomials.

Implementation of this proof method into Theorema is quite easy since the algorithm for computing Groebner bases is already available as a Mathematica function.

Load Groebner Bases Prover

By the subsequent command, the Theorema Groebner Bases Prover is loaded:

\(Needs[
      "Theorema`Provers`UserProvers`GroebnerBasesProver`"]; $TmaProofPresentation\  = \ 100; \)

Example

Here is an example of a universally quantified boolean combination of equalities over the complex numbers:

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

A proof for this formula can be generated  by the following call:

Prove[Formula["Test"], using -> {}, 
      by -> GroebnerBasesProver]

The result of calling the prover is a proof of the proposition. The proof is stored in an extra notebook with name 'Untitled-...'. (If you are a Theorema alpha tester you can execute the above command and actually generate this notebook. For the other readers the file is stored under the name Theorema-Demo-1999- Proof-by-Groebner-Bases.nb or, alternatively, the file Theorema-Demo-1999-Proof-by-Groebner-Bases.ps.)

Example: Proving Combinatorial Identities by Zeilberger / Paule

The Purpose of this Example

The next example is along the same lines as the Groebner bases proving method. This time, the class of theorems one is interested in is the class of combinatorial identities (terms involving elementary functions over the natural numbers and the summation quantifier). In the past 10 years, by Gosper, Zeilberger, Paule, and others, a powerful special automated proving technique has also been developed  for this class of formulae,  see the literature given in P. Paule's computer-solution of Problem 94-2, SIAM REVIEW Vol.37 (1995), 105-106.

Again, the method is based on some quite heavy mathematical machinery. Its proof has to be established once and for all and, then, it can be used for proving an infinite class of - quite nontrivial and hard - combinatorial identities.

The implementation of this method in Theorema together with essential mathematical improvements of the method was done by P. Paule and M. Schorn.

Load Prover

We first load the prover:

Needs["Theorema`Provers`PauleSchorn`Simplifier`"]

We also have to load a couple of built-in algorithms for basic logical and mathematical operators.

Built–in["PauleSchorn",
	({{Built–in["Quantifiers"]}, {Built–in["Operators"]}, {Built–in["Numbers"]}, {Built–in["Number Domains"]}, {Built–in["Forward Difference"]}})]

Use[Built–in["PauleSchorn"]];
\(\(FormatVariables[
	FontWeight -> "Plain"\ , 
	
        FontSlant -> "Italic"
];\)\)
\(FormatArbitraryButFixedConstants[
	
      FontWeight -> "Plain"\ , 
	
      FontSlant -> "Plain"
]\)

Invent and Prove

We start with one of the most elementary (and historically important) formula in the class of combinatorial identities:

Formula[\("Gauss", 
	
      ∑\+\(k = 0, …, n\)k\)]

The following call does actually more than just proving a theorem about the Gauss sum: It invents a closed form for this sum and proves it.  In the present version, the proof consists in producing a summation-free expression that can be considered as a "test expression". If this expression can be simplified to 1, the closed form is correct. Hence, in the present version, in order to complete the proof, the user must call a simplifier for checking whether the output test expression reduces to 1. Also, in the present version, the proof text is shown right in the Mathematica notebook from which the prover is called, i.e. here it is shown just below the call. A future version of this prover will be adjusted to the usual style of the Theorema provers.

Prove[Formula["Gauss"], by -> PauleSchorn–Telescope, 
      built–in -> Built–in["PauleSchorn"]]

The simplification can be done by called Mathematica's simplifier:

System`Simplify[(((1/2) k (1+k)-(1/2) (-1+k) k)/k)]

A Nontrivial Example

Now we show another example, which shows the mathematical power of the Gosper-Zeilberger-Paule-prover: The problem of constructing a closed form for the input expression in this example 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.

Here is the expression:

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

Here is the call of the prover:

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

Again, the simplification can be accomplished by calling Mathematica's simplifier:

System`FullSimplify[(((((((-1))^(1+k)) (2^(1+-2 (1+k))) (2 (1+k))! (2+k))/((1+k)! (2+k)! (-1+2 (1+k))))-(((((-1))^k) (2^(1+-2 k)) (2 k)! (1+k))/(k! (1+k)! (-1+2 k))))/((-(((-1))^k) (2^(-2 k)) (2 k)! (1+4 k))/(k! (1+k)! (-1+2 k))))]

Computing and Mathematica within Theorema

The Purpose of this Section

In this section, we demonstrate how Theorema can be used in a way similar to Mathematica but with some additional functionalities:

We demonstrate how all Mathematica functions can also be called from within Theorema.

We demonstrate how, in Theorema, the language construct "functor" can be used. This is an important construct that helps in structuring large mathematical  theories. The functor construct is not available in Mathematica.

Finally, we demonstrate how Theorema can be used in a special interactive style (which we call "computational sessions") that resembles the traditional input-evaluate-output style of Mathematica sessions. Note, however, that the syntax of Theorema (which we think is much closer to the usual syntax in mathematics textbooks) is preserved also in the computational sessions of Theorema. In particular, for example, the Theorema notation for sets and operations on sets is exactly the one of set theory textbooks. This is in sharp contrast to Mathematica that uses set notation for tuples, which is quite confusing for mathematicians.

Load Additionals

We first load a couple of built-in operations and special functions for demonstrating the functor construct.

Use[{}]

InitializeGlobals[Evaluator -> EvaluateFromInnermost]; 
    UseAlso[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], 
        Built–in["Sets"]⟩]

ClearAll[LM]LM[p_Plus] := Last[p]LM[p_Times] := pLM[p_Power] := pLM[v_Symbol] := vLM := c /; NumberQ[c]

ClearAll[PP]
PP[Times[c_, pp___]] := Times[pp] /; NumberQ[c]
PP[c_] := 1 /; NumberQ[c]
PP[m_] := m

ClearAll[coefficient]
coefficient[Times[c_, pp___]] := c /; NumberQ[c]
coefficient[c_] := c /; NumberQ[c]
coefficient[m_] := 1

Remove[𝒫]

Make Mathematica Functions Accessible

Here is the way how functions form the Mathematica library or functions that had been defined by the user within Mathematica, like 'Expand', 'PolynomialGCD', etc. can be made accessible, with new names, from within Theorema.

Built–in["Mathematica",
	({{polynomial -> Expand}, {monomial -> Expand}, {polynomial–gcd -> PolynomialGCD}, {polynomial–lcm -> PolynomialLCM}, {leading–monomial -> LM}, {power–product -> PP}, {are–equal -> SameQ}})]

UseAlso[
      ⟨Built–in["Mathematica"]
          ⟩]

Define a Functor

Functors, like in ML etc., are a very powerful tool for building up and computing in 'towers' of abstract domains. By adding functors to Theorema, everything that can be done e.g. in the system Axiom, can be done in Theorema. Here is a first trivial functor that has no parameters and combines a couple of operations on polynomials (like '+', ..., 'gcd', etc.) in one "domain":

Definition["Mathematica Polynomials",
	Mathematica–Polynomials[]=Functor[𝒫,any[p, q, m, n],
	({{𝕤 = ⟨⟩}, {({{(Underscript[0, 𝒫]) = 0}, {\(p\( + \+𝒫\)q = 
                            polynomial[p + q]\)}, {\(\(-\+𝒫 q\) = 
                            polynomial[\(-q\)]\)}, {\(p\( - \+𝒫\)q = 
                            polynomial[p - q]\)}, {(Underscript[1, 𝒫]) = 1}, {\(m\(*\+𝒫\)n = monomial[m\ *\ n]\)}, {\(m\(/\+𝒫\)n = monomial[m\ /\ n]\)}, {(m (Underscript[∣ , 𝒫])n)⟺(are–equal[power–product[m], 
                                power–product[
                                  polynomial–gcd[m, n]]])}, {(Underscript[gcd, 𝒫])[m, n] = 
                            polynomial–gcd[m, n]}, {(Underscript[lcm, 𝒫])[m, n] = 
                            polynomial–lcm[m, n]}, {(Underscript[ldm, 𝒫])[p] = 
                            leading–monomial[p]}, {(Underscript[rest, 𝒫])[p] = 
                            polynomial[p - leading–monomial[p]]}, {(Underscript[poly, 𝒫])[m, p] = 
                            polynomial[m + p]}})}})
	]]

Compute in a Domain Defined by a Functor

Here is a call of the functor "Mathematica–Polynomials" that creates a domain with name "ℙ":

Definition[\("ℙ", 
	
      ℙ = Mathematica–Polynomials[]\)]

The definition of the domain 'ℙ' and the functor 'Mathematica-Polynomials' can now be combined in a theory:

Theory["T",
	({{Definition["ℙ"]}, {Definition["Mathematica Polynomials"]}})]

Now we can compute in the domain 'ℙ' by calling operations like '+', '*', etc. but with the distinctive subscript 'ℙ' that indicates that these operations are the ones defined in 'ℙ' (which may be completely different from the "ordinary" built-in operations of Theorema and from the operations in other domains generated by other functors.)  In order to compute, for example,

\(\((\(x\^2\) y\^2)\)\(*\+ℙ\)\((\(-13\)/4\ x\ y)
        \)\)

we must, of course, tell Theorema that we want it to use (only) the Theory["T"]:

\(Compute[
      \((\(x\^2\) y\^2)\)\(*\+ℙ\)\((\(-13\)/4\ x\ y)\), 
      using -> Theory["T"]]\)

In addition to the result, we also obtain a trace of the most important steps in the evaluation. If we do not want to see this, we can turn the trace off by

SetGlobals[TraceLevel -> 0]

\(Compute[
      \((\(x\^2\) y\^2)\) /\+ℙ\((\(-13\)/4\ x\ y)\), 
      using -> Theory["T"]]\)

Compute[
      ((x^2) (y^2)) (Underscript[∣ , ℙ])(
          -13/4 x y), using -> Theory["T"]]

Compute[
      (x y) (Underscript[∣ , ℙ])(
          -13/4 (x^2) y), using -> Theory["T"]]

Extend a Functor

Now we demonstrate how a functor can be "extended" by adding more functions. This functor has a parameter: It depends on the domain 'ℛ' which we want to extend:

Definition["Reduction Domain",any[𝒫],
	Reduction–Domain[𝒫]=Functor[⟨ℛ, 
                extends[𝒫]⟩,any[p, q],
	({{𝕤 = ⟨SP ∶ ℛ\[Cross]ℛ -> ℛ⟩}, {\(SP\+ℛ[p, q] = 
                      where[
	
                        L = lcm\+𝒫[ldm\+𝒫[p], 
                            ldm\+𝒫[q]], 
                        u = \((L\(/\+𝒫\)\((ldm\+𝒫[p])\))\), 
                        v = \((L\(/\+𝒫\)\((ldm\+𝒫[q])\))\), 
	
                        u\(*\+𝒫\)rest\+𝒫[
                              p]\( - \+𝒫\)v\(*\+𝒫\)rest\+𝒫[q]]\)}})
	]]

The "reduction domain" of a given domain ℛ is identical to ℛ but provides also the function 'SP' (S-polynomial), which is defined exclusively in terms of the operations available in ℛ! The definition of SP is, hence, completely independent of the particular instance of the domain ℛ.

Now we call this functor for generating the reduction domain of the Mathematica polynomials:

Definition[\("RDMP", 
	
        ℙ = 
          Reduction–Domain[Mathematica–Polynomials[]]\)]

We now combine all definitions that we need for computing in this domain in a theory:

Theory["RDMP",
	({{Definition["RDMP"]}, {Definition["Mathematica Polynomials"]}, {Definition["Reduction Domain"]}})]

\(Compute[
      \((x\ y\^2 - 3  x\ y\  + \ x\^2)\)\( + \+ℙ\)\((
          x\^2\ y\^2 + 3  x\ y\  + \ x\^2 - 3  x)\), 
      using -> Theory["RDMP"]]\)

Compute[
      (Underscript[SP, ℙ])[(x (y^3) - 3  x y  +  (x^2)), 
        ((x^2) (y^2) + 3  x y  +  (x^2) - 3  x)], 
      using -> Theory["RDMP"]]

Theorema Computational Sessions

In a Theorema computational session, like in a Mathematica session, all definitions are automatically adjoined to a global knowledge base and 'Compute' need not be called explicitly. We enter a computational session by entering:

ComputationalSession[]

As an example, let's now do some computations with sets:

\({\ i\( | \+\(i ∈ {1, 2, 3}\)\)}\)

\({\ \((2\ i)\)\( | \+\(i = 1, …, 3\)\)}\)

\({i  |\+\(i = 1, …, 20\)is–prime[i]}\)

{2, 3, 1, 2, 3} = {1, 2, 3, 3, 3}

Note that this is true because the two terms, in fact, denote the same set:

{2, 3, 1, 2, 3}

{1, 2, 3, 3, 3}

{1, 2, 1, 3} = {2, 1, 4, 3}

2 ∈ {2, 1, 2, 4}

Now we define two operations on sets that are not built in:

any[IsSet[A, B]]∶
	({{\(A⊖B := {\ 
                x  |\+\(x ∈ A\)\((x ∉ B)\)}\)}, {A ⊆ B := 
              (Underscript[∀ , x ∈ A])x ∈ B}})

Note that these definitions are exactly in the style used in math textbooks, i.e. in Theorema one can "compute" with ordinary mathematical formulae (as long as these formulae have an algorithmic meaning):

{2, 3, 1, 3}⊖{3, 5}

Note that the new operator, before evaluating, checks whether the parameter terms denote sets. For example,

2⊖3

just stays unevaluated because the above definition of '⊖' was restricted to sets.

{3, 2, 5} ⊆ {1, 2, 3, 4, 5}

One can also check the type of objects:

is–set[{2, 3, 2}]

is–set[{2, 3}]

is–tuple[{2, 3, 2}]

is–tuple[⟨2, 3, 2⟩]

Some operators denote various different functions depending on the type of the objects provided as input:

\[LeftBracketingBar]⟨2, 3, 2
        ⟩\[RightBracketingBar]

\[LeftBracketingBar]{2, 3, 2}\[RightBracketingBar]

\[LeftBracketingBar]-3\[RightBracketingBar]

The function 'æ' ("an element in") produces an element from a (non-empty) set:

æ[{3}]

Here is a property of the power set function that uses the function æ:

any[is–set[A]]∶
	({{𝔓[A] := {{}} ⇐ (A = {})}, {\(𝔓[A] := 
              where[a = æ[A], P = 𝔓[A⊖{a}], 
                \ 
	P ⋃ {\(({a} ⋃ B)\) |\+\(B ∈ P\)}]
                \)}})

This property could be proved by the set prover. For finite sets A  this property can also be viewed as a recursive algorithm for computing the power set of A:

𝔓[{}]

𝔓[{3}]

\(\(𝔓[{1, 3}]
\)\)

𝔓[{1, 3, 4, 8}]

We can go back to a standard session of Theorema by entering:

EndComputationalSession[]

Now the information on the power set function is not any more available:

𝔓[{1, 3, 4, 8}]

Appendix:
Proofs

GCD

Divides Difference

Prove:

under the assumptions:

We assume

and show

We prove the individual conjunctive parts of (2):

Proof of (2.1) (Subscript[d, 0])∣(Subscript[m, 0])-(Subscript[n, 0]):

Formula (1.1), by (div:), implies:

By (3) we can take appropriate values such that:

Formula (1.2), by (div:), implies:

By (5) we can take appropriate values such that:

By modus ponens, from (6), (4) and an appropriate instance of (distr) follows:

Formula (2.1), using (div:), is implied by:

Formula (8) is proved because (7) is an instance of it.

Proof of (2.2) (Subscript[d, 0])∣(Subscript[n, 0]):

Formula (2.2) is true because it is identical to (1.2).

Analysis

4-ary Limit

Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (l4:), implies:

Formula (1.2), by (l4:), implies:

Formula (2), using (l4:), is implied by:

We assume

and show

Formula (6), by (≥max ), implies:

Formula (8.1), by (3), implies:

Formula (8.2), by (4), implies:

Formula (7), using (+:), is implied by:

|((Subscript[f, 0])[(Subscript[n, 0])]+(Subscript[g, 0])[(Subscript[n, 0])])-((Subscript[a, 0])+(Subscript[b, 0]))|<(Subscript[δ, 0])+(Subscript[ϵ, 0]),

which, using (| + |), is implied by:

We prove the individual conjunctive parts of (11):

Proof of (11.1) |(Subscript[f, 0])[(Subscript[n, 0])]-(Subscript[a, 0])|<(Subscript[δ, 0]):

Formula (11.1) is true because it is identical to (9).

Proof of (11.2) |(Subscript[g, 0])[(Subscript[n, 0])]-(Subscript[b, 0])|<(Subscript[ϵ, 0]):

Formula (11.2) is true because it is identical to (10).

3-ary Limit

Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (l3:), implies:

By (3) we can take appropriate values such that:

Formula (1.2), by (l3:), implies:

By (5) we can take appropriate values such that:

By modus ponens, from (6), (4) and an appropriate instance of (lim+) follows:

Formula (2), using (l3:), is implied by:

Formula (8) is proved because (7) is an instance of it.

2-ary Limit

Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (l2:), implies:

Formula (1.2), by (l2:), implies:

Formula (2), using (l2:), is implied by:

We assume

and show

Formula (6), by (4), implies:

Formula (6), by (3), implies:

Formula (6), by (/2>), implies:

Formula (10), by (4), implies:

Formula (10), by (3), implies:

Formula (7), using (l3+), is implied by:

We prove the individual conjunctive parts of (13):

Proof of (13.1) limit[(Subscript[f, 0]),(Subscript[a, 0]),(((Subscript[ϵ, 0]))/2)]:

Formula (13.1) is true because it is identical to (12).

Proof of (13.2) limit[(Subscript[g, 0]),(Subscript[b, 0]),(((Subscript[ϵ, 0]))/2)]:

Formula (13.2) is true because it is identical to (11).

Continuity of Product

Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (c4:), implies:

Formula (1.2), by (c4:), implies:

Formula (2), using (c4:), is implied by:

We assume

and show

Formula (6), by (min<), implies:

Formula (8.1), by (3), implies:

Formula (8.2), by (4), implies:

Formula (7), using (f*g), is implied by:

|(Subscript[f1, 0])[(Subscript[x, 0])]*(Subscript[f2, 0])[(Subscript[x, 0])]-(Subscript[f1, 0])[(Subscript[y, 0])]*(Subscript[f2, 0])[(Subscript[y, 0])]|<ϵ(Subscript[1, 0])*(ϵ(Subscript[2, 0])+|(Subscript[f2, 0])[(Subscript[x, 0])]|)+|(Subscript[f1, 0])[(Subscript[x, 0])]|*ϵ(Subscript[2, 0]),

which, using (| * |), is implied by:

We prove the individual conjunctive parts of (11):

Proof of (11.1) |(Subscript[f1, 0])[(Subscript[x, 0])]-(Subscript[f1, 0])[(Subscript[y, 0])]|<ϵ(Subscript[1, 0]):

Formula (11.1) is true because it is identical to (9).

Proof of (11.2) |(Subscript[f2, 0])[(Subscript[x, 0])]-(Subscript[f2, 0])[(Subscript[y, 0])]|<ϵ(Subscript[2, 0]):

Formula (11.2) is true because it is identical to (10).

"Prove - Compute - Solve"

2-ary Limit with PCS

Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (l), implies

By (3) we can take an appropriate Skolem function such that:

Formula (1.2), by (l), implies:

By (5) we can take an appropriate Skolem function such that:

Formula (2), using (l), is implied by:

We assume

and have to find an N* such that

Formula (9), using (f+g), is implied by:

Formula (10), using (dist+), is proved if we can find δ*, ϵ* such that

Formula (11), using (6) and (4) is,  implied by:

Example: Set Theory Proving

Classes Modulo Symmetric Predicates

Prove:

under the assumptions:

We assume

and show

We assume

and show

Formula (3), by (⌊ ⌋:), implies:

From (5) we know

Formula (1), by (symm:), implies:

Formula (6), by (7), implies:

Formula (4), using (⌊ ⌋:), is implied by:

(Subscript[b, 0])∈{b(Underscript[|, b ]) (Subscript[∼ , 0])[b,(Subscript[a, 0])]},

which, using (7), is implied by:

In order to prove (9) we have to show:

Formula (10) is true because it is identical to (6).

Commutativity of Addition

Proof Attempt

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( + = )fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ( + = ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (1) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

0+(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])+0 =by ( +0:)

(Subscript[n, 1])⌋

Hence, it is sufficient to prove:

We prove (5) by  induction on n.

Induction Base:

A proof by simplification of (6) works.

Simplification of the lhs term:

0 + 0 =by ( +0:)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (8) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[n, 2])]) =by ( + .:)

(SuperPlus[(0+(Subscript[n, 2]))]) =by (7)

(SuperPlus[(Subscript[n, 2])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 2])])⌋

Alternative proof 2: pending

Pending proof of (1).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in (3) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(Subscript[n, 3])⌋

Simplification of the rhs term:

(Subscript[n, 3])+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[((Subscript[n, 3])+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

We try to prove (10) by  induction on n.

Induction Base:

We simplify (11).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =by ( +0:)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(0+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (14)fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of (13).

Alternative proof 2: failed

We try to prove (3) by  induction on n.

Induction Base:

We simplify (15).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =by ( +0:)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

0+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[(0+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (18)fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of (17).

Cascade: Lemmata Generation

First Step: A Failing Proof of Commutativity of Addition

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( + = )fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ( + = ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (1) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

0+(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])+0 =by ( +0:)

(Subscript[n, 1])⌋

Hence, it is sufficient to prove:

We prove (5) by  induction on n.

Induction Base:

A proof by simplification of (6) works.

Simplification of the lhs term:

0 + 0 =by ( +0:)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (8) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[n, 2])]) =by ( + .:)

(SuperPlus[(0+(Subscript[n, 2]))]) =by (7)

(SuperPlus[(Subscript[n, 2])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 2])])⌋

Alternative proof 2: pending

Pending proof of (1).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in (3) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(Subscript[n, 3])⌋

Simplification of the rhs term:

(Subscript[n, 3])+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[((Subscript[n, 3])+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

We try to prove (10) by  induction on n.

Induction Base:

We simplify (11).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =by ( +0:)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(0+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (14)fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of (13).

Alternative proof 2: failed

We try to prove (3) by  induction on n.

Induction Base:

We simplify (15).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =by ( +0:)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

0+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[(0+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (18)fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of (17).

Second Step: A First Automatically Generated Lemma

Prove:

under the assumptions:

We prove (19) by  induction on m.

Induction Base:

A proof by simplification of (20) works.

Simplification of the lhs term:

0 + 0 =by ( +0:)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (22) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[(0+(Subscript[m, 1]))]) =by (21)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])⌋

Third Step:  Proof Attempt of Commutativity of Addition With Increased Knowledge

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( + = )fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ( + = ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (20) all variables arbitrary but fixed and prove:

A proof by simplification of (23) works.

Simplification of the lhs term:

0+(Subscript[n, 1]) =by (19)

(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])+0 =by ( +0:)

(Subscript[n, 1])⌋

Alternative proof 2: pending

Pending proof of (20).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in (22) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(Subscript[n, 2])⌋

Simplification of the rhs term:

(Subscript[n, 2])+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[((Subscript[n, 2])+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

We try to prove (25) by  induction on n.

Induction Base:

A proof by simplification of (26) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =by ( +0:)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(0+(Subscript[m, 1]))]) =by (19)

(SuperPlus[(Subscript[m, 1])])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We simplify (28).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(SuperPlus[(Subscript[n, 3])]) =by ( + .:)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 3]))]) =by (27)

(SuperPlus[((SuperPlus[((Subscript[n, 3])+(Subscript[m, 1]))]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (29)fails.(No applicable inference rule was found.)

Alternative proof 2: failed

We try to prove (22) by  induction on n.

Induction Base:

A proof by simplification of (30) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =by ( +0:)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

0+(SuperPlus[(Subscript[m, 1])]) =by (19)

(SuperPlus[(Subscript[m, 1])])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We simplify (32).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(SuperPlus[(Subscript[n, 4])]) =by ( + .:)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))]) =by (31)

(SuperPlus[((Subscript[n, 4])+(SuperPlus[(Subscript[m, 1])]))]) =by ( + .:)

(SuperPlus[((SuperPlus[((Subscript[n, 4])+(Subscript[m, 1]))]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 4])])+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[((SuperPlus[(Subscript[n, 4])])+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (33)fails.(No applicable inference rule was found.)

Fourth Step:  A Second Automatically Generated Lemma

Prove:

under the assumptions:

We prove (34) by  induction on n.

Induction Base:

We take in (35) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

\(0\^+\)+(Subscript[m, 1])⌋

Simplification of the rhs term:

(SuperPlus[(0+(Subscript[m, 1]))]) =by (19)

(SuperPlus[(Subscript[m, 1])])⌋

Hence, it is sufficient to prove:

We prove (39) by  induction on m.

Induction Base:

A proof by simplification of (40) works.

Simplification of the lhs term:

\(\(0\^+\) + 0\) =by ( +0:)

\(\(0\^+\)\)⌋

Simplification of the rhs term:

\(\(0\^+\)\)⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (42) works.

Simplification of the lhs term:

\(0\^+\)+(SuperPlus[(Subscript[m, 2])]) =by ( + .:)

(SuperPlus[(\(0\^+\)+(Subscript[m, 2]))]) =by (41)

(SuperPlus[((SuperPlus[(Subscript[m, 2])]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 2])]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (37) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[n, 1])]))])+(Subscript[m, 3])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[(Subscript[n, 1])])+(Subscript[m, 3]))]) =by (36)

(SuperPlus[((SuperPlus[((Subscript[n, 1])+(Subscript[m, 3]))]))])⌋

Hence, it is sufficient to prove:

We prove (44) by  induction on m.

Induction Base:

A proof by simplification of (45) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[n, 1])]))])+0 =by ( +0:)

(SuperPlus[((SuperPlus[(Subscript[n, 1])]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[((Subscript[n, 1])+0)]))]) =by ( +0:)

(SuperPlus[((SuperPlus[(Subscript[n, 1])]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (47) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[n, 1])]))])+(SuperPlus[(Subscript[m, 4])]) =by ( + .:)

(SuperPlus[((SuperPlus[((SuperPlus[(Subscript[n, 1])]))])+(Subscript[m, 4]))]) =by (46)

(SuperPlus[((SuperPlus[((SuperPlus[((Subscript[n, 1])+(Subscript[m, 4]))]))]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[((Subscript[n, 1])+(SuperPlus[(Subscript[m, 4])]))]))]) =by ( + .:)

(SuperPlus[((SuperPlus[((SuperPlus[((Subscript[n, 1])+(Subscript[m, 4]))]))]))])⌋

Fifth Step: A Successful Proof of Commutativity of Addition

Prove:

under the assumptions:

We prove ( + = ) by  induction on m.

Induction Base:

We take in (35) all variables arbitrary but fixed and prove:

A proof by simplification of (38) works.

Simplification of the lhs term:

0+(Subscript[n, 1]) =by (19)

(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])+0 =by ( +0:)

(Subscript[n, 1])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (37) all variables arbitrary but fixed and prove:

A proof by simplification of (39) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(Subscript[n, 2]) =by (34)

(SuperPlus[((Subscript[m, 1])+(Subscript[n, 2]))]) =by (36)

(SuperPlus[((Subscript[n, 2])+(Subscript[m, 1]))])⌋

Simplification of the rhs term:

(Subscript[n, 2])+(SuperPlus[(Subscript[m, 1])]) =by ( + .:)

(SuperPlus[((Subscript[n, 2])+(Subscript[m, 1]))])⌋

Associativity of Multiplication

Using Associativity and Commutativity as Part of the Knowledge Base

Prove:

under the assumptions:

We prove (( * ) * ) by  induction on m.

Induction Base:

We take in (1) all variables arbitrary but fixed and prove:

A proof by simplification of (4) works.

Simplification of the lhs term:

(0*(Subscript[n, 1]))*(Subscript[p, 1]) =by (0*)

0*(Subscript[p, 1]) =by (0*)

0⌋

Simplification of the rhs term:

0*((Subscript[n, 1])*(Subscript[p, 1])) =by (0*)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (3) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2]))*(Subscript[p, 2]) =by ( ^+*)

((Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]))*(Subscript[p, 2]) =by ( + )

((Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])*((Subscript[n, 2])*(Subscript[p, 2])) =by ( ^+*)

(Subscript[m, 1])*((Subscript[n, 2])*(Subscript[p, 2]))+(Subscript[n, 2])*(Subscript[p, 2]) =by (2)

((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])+(Subscript[n, 2])*(Subscript[p, 2]) =by ( + )

(Subscript[n, 2])*(Subscript[p, 2])+((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Hence, it is sufficient to prove:

We prove (6) by  induction on n.

Induction Base:

We take in (7) all variables arbitrary but fixed and prove:

A proof by simplification of (10) works.

Simplification of the lhs term:

(0+(Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

(0 + 0)*(Subscript[p, 3]) =by ( +0)

0*(Subscript[p, 3]) =by (0*)

0⌋

Simplification of the rhs term:

0*(Subscript[p, 3])+((Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

0*(Subscript[p, 3])+0*(Subscript[p, 3]) =by (0*)

0+0*(Subscript[p, 3]) =by (0*)

0 + 0 =by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We prove (9) by  induction on p.

Induction Base:

A proof by simplification of (17) works.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*0 =by ( *0)

0⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*0+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*0 =by (2)

(SuperPlus[(Subscript[n, 3])])*0+(Subscript[m, 1])*((SuperPlus[(Subscript[n, 3])])*0) =by ( *0)

0+(Subscript[m, 1])*((SuperPlus[(Subscript[n, 3])])*0) =by ( *0)

0+(Subscript[m, 1])*0 =by ( *0)

0 + 0 =by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (19) works.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by (18)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by (^++ )

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))]) =by ( + ^+)

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(SuperPlus[(Subscript[p, 6])])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by ( + ^+)

(SuperPlus[(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))])+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by (^++ )

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =by ( + )

(SuperPlus[((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =by (( + ) + )

(SuperPlus[(((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =by ( + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Using Associativity and Commutativity as Inference Rules

Prove:

under the assumptions:

We prove (( * ) * ) by  induction on m.

Induction Base:

We take in (1) all variables arbitrary but fixed and prove:

A proof by simplification of (4) works.

Simplification of the lhs term:

(0*(Subscript[n, 1]))*(Subscript[p, 1]) =by (0*)

0*(Subscript[p, 1]) =by (0*)

0⌋

Simplification of the rhs term:

0*((Subscript[n, 1])*(Subscript[p, 1])) =by (0*)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (3) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2]))*(Subscript[p, 2]) =by ( ^+*)

((Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]))*(Subscript[p, 2]) =by (Special Simpl )

((Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])*((Subscript[n, 2])*(Subscript[p, 2])) =by ( ^+*)

(Subscript[m, 1])*((Subscript[n, 2])*(Subscript[p, 2]))+(Subscript[n, 2])*(Subscript[p, 2]) =by (2)

((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])+(Subscript[n, 2])*(Subscript[p, 2]) =by (Special Simpl )

(Subscript[n, 2])*(Subscript[p, 2])+((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Hence, it is sufficient to prove:

We prove (6) by  induction on n.

Induction Base:

We take in (7) all variables arbitrary but fixed and prove:

A proof by simplification of (10) works.

Simplification of the lhs term:

(0+(Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

(0 + 0)*(Subscript[p, 3]) =by ( +0)

0*(Subscript[p, 3]) =by (0*)

0⌋

Simplification of the rhs term:

0*(Subscript[p, 3])+((Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

0*(Subscript[p, 3])+0*(Subscript[p, 3]) =by (0*)

0+0*(Subscript[p, 3]) =by (0*)

0 + 0 =by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (9) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by (Special Simpl)

((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by ( *  ^+)

(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by (Special Simpl)

(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))])*(Subscript[p, 4]) =by (Special Simpl)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))])*(Subscript[p, 4]) =by ( ^+*)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4])+(Subscript[p, 4]) =by (Special Simpl )

(Subscript[p, 4])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by (Special Simpl)

((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4])+(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4]) =by ( *  ^+)

((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4])+(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4]) =by (Special Simpl)

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =by ( ^+*)

((Subscript[n, 3])*(Subscript[p, 4])+(Subscript[p, 4]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =by (Special Simpl )

(Subscript[p, 4])+((Subscript[n, 3])*(Subscript[p, 4])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]))⌋

Hence, it is sufficient to prove:

We prove (12) by  induction on p.

Induction Base:

A proof by simplification of (13) works.

Simplification of the lhs term:

0+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*0 =by ( *0)

0 + 0⌋

Simplification of the rhs term:

0+((Subscript[n, 3])*0+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0) =by ( *0)

0+(0+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0) =by ( *0)

0 + (0 + 0) =by (Special Simpl)

(0 + 0) + 0 =by ( +0)

0 + 0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (15) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])]) =by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])]) =by ( *  ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3]))))+(SuperPlus[(Subscript[p, 5])]) =by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(SuperPlus[(Subscript[p, 5])]) =by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(Subscript[p, 5]))]) =by (Special Simpl)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =by (14)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =by (Special Simpl )

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])) =by (Special Simpl)

(Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =by ( *  ^+)

((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =by (Special Simpl)

(Subscript[n, 3])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =by ( *  ^+)

(Subscript[n, 3])+((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(SuperPlus[(Subscript[p, 5])]) =by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(Subscript[p, 5]))]) =by (Special Simpl )

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))])⌋

Proving Booleans of Equalities by Groebner Bases

Universally Quantified Boolean Combination of Equalities Over the Complex Numbers:

Prove:

with no assumptions.

Proved.

The Theorem is proved by the Groebner Bases method.      

      The formula in the scope of the universal quantifier is transformed into an equivalent formula that is a conjunction of disjunctions of equalities and negated equalities. The universal quantifier can then be distributed over the individual parts of the conjunction. By this, we obtain:

Independent proof problems:

We now prove the above individual problems separately:

Proof of (.1):

This proof problem has the following structure:

where

({{Poly[1] =, -3*x+(x^2)*y}, {Poly[2] =, x+y+x*y}, {Poly[3] =, (x^2)+(-x*y)+(x^2)*y+-2*(y^2)+-2*x*(y^2)}})

(.1.structure) is equivalent to

(.1.implication) is equivalent to

By introducing the slack variable(s)

{ξ}

(.1.not-exists) is transformed into the equivalent formula

Hence, we see that the proof problem is transformed into the question on whether or not a system of polynomial equations has a solution or not. This question can be answered by checking whether or not the (reduced) Groebner basis of

{Poly[1], Poly[2], -1 + ξ Poly[3]}

is exactly {1}.                  

Hence, we compute the Groebner basis for the following polynomial list:

\({\(-1\) + x\^2\ ξ + \(-x\)\ y\ ξ + 
        x\^2\ y\ ξ + \(-2\)\ y\^2\ ξ + \(-2\)\ x\ y\^2\ ξ, \(-3\)\ x + x\^2\ y, x + y + x\ y}\)

The Groebner basis:

{1}

Hence, (.1) is proved.

Proof of (.2):

This proof problem has the following structure:

where

({{Poly[1] =, -3*x+(x^2)*y}, {Poly[2] =, x+y+x*y}, {Poly[3] =, 3*x+(x^2)*y}, {Poly[4] =, -2*(x^2)+-7*x*y+(x^2)*y+(x^3)*y+-2*(y^2)+-2*x*(y^2)+2*(x^2)*(y^2)}})

(.2.structure) is equivalent to

(.2.implication) is equivalent to

By introducing the slack variable(s)

{ξ1, ξ2}

(.2.not-exists) is transformed into the equivalent formula

Hence, we see that the proof problem is transformed into the question on whether or not a system of polynomial equations has a solution or not. This question can be answered by checking whether or not the (reduced) Groebner basis of

{Poly[1], 
      Poly[2], -1 + ξ1 Poly[3], -1 + ξ2 Poly[
            4]}

is exactly {1}.                  

Hence, we compute the Groebner basis for the following polynomial list:

\({\(-1\) + 3\ x\ ξ1 + 
        x\^2\ y\ ξ1, \(-1\) + \(-2\)\ x\^2\ ξ2 + \(-7\)\ x\ y\ ξ2 + x\^2\ y\ ξ2 + 
        x\^3\ y\ ξ2 + \(-2\)\ y\^2\ ξ2 + \(-2\)\ x\ y\^2\ ξ2 + 
        2\ x\^2\ y\^2\ ξ2, \(-3\)\ x + x\^2\ y, x + y + x\ y}\)

The Groebner basis:

{1}

Hence, (.2) is proved.

Since all of the individual subtheorems are proved, the original formula is proved.