Theorem Proving

Currently, when talking about 'theorem proving', we think of yes/no(/unknown) answers, rather than giving a complete proof. This is simply because of the complexity and difficulty of creating a human readable proof. Later (maybe in some years, but not for any forthcoming versions of GeoGebra) we may extend this definition.

"Is line x parallel to line y?", "are A, B and C collinear?". GeoGebra can currently do such things by numerical calculations, but in some cases these are unexact or may give the wrong answer.

Overview and brainstorming

GeoGebra needs a theorem proving subsystem, since such questions may be difficult to answer by using an easy way. Basically, if there is a thesis (T={t}), it may be a consequence of hypotheses (H). In general, a prover with the input t can create the needed set H (by analyzing the dependency structure of the construction object tree), and outputs if H=>T is true , H=>T is generally true (i.e. true if some conditions are also true), H=>T is false or H=>T is unknown. We plan to use such a prover for the following GeoGebra tasks:

• Checking boolean expressions. Here t is the boolean expression.
• Exploring relations between two objects (Relation tool and command). Here several theses can be an input for the prover; for given objects x and y, t can be x==y, x is parallel to y, x is perpendicular to y, x lies on y, x is a tangent for y; and vice versa.
• Creating exercises for constructions. Here there is a construction created by the teacher with some hidden objects X as the correct result of the exercise. The student creates her solution which is the set of objects Y. Now t="X==Y".
• Continuity checks. (Explanation needed.)

The prover itself is a "clever machine" which tries to decide how it can prove the input. There may be at least four different subsystems which could offer different methods for proving. Of course, it is possible that certain techniques will be merged in a simple tool, preferably ​OpenGeoProver. Some possible subsystems:

1. Stochastic method by checking the thesis for N tests.
   1. Tomas Recio's idea is to use the 2D Bezout theorem to ensure a limit for N (depending on the object types of the underlying construction itself).
   2. Tam already started to implement a checker for N>1. (Reference needed.) If Tomas' idea can ensure a limit, then set N, if it cannot, then set N to a default value.
   3. It is already implemented for N=1 for the Relation tool, and for continuity checks. (References needed.) Now call this method N times as calculated in a. or b.
2. Rewrite the construction to a better representation for an algebraic solver. OpenGeoProver will use this better representation and it creates a set of polynomials by using several tricks (based mainly on Chou's methods). The polynomials are then used as an input for Wu's or the Gröbner basis method, and with the output the extra conditions are also returned (non-degeneracy conditions, "NDG"). OpenGeoProver will be an adequate subsystem for this since it has a very similar kernel to GCLC, developed by Predrag Janicic since 1996.
3. Symbolic way. We can create the symbolic equation for each object by extending the data structure of GeoGebra. This basically means that all objects will be appended by such parametric data which describe the appropriate numbers with expressions. E.g. assume that a regular triangle is drawn with A(0,0), B(1,0), C(1/2,sqrt(3)/2). Now the y coordinate of C will be stored as an expression, not just a floating point number. If someone draws the line BC, then it will also be stored in its normal form: sqrt(3)/2*x+(1/2)*y=sqrt(3)/2. This is the most difficult way since the source code must be extended at several places. To check if a statement is true, we have to check the relations of the expressions in a symbolic way (by using the underlying CAS, for example). However Sergio already implemented most of the work for this in his LocusLineEquation branch in geogebra.kernel.locusequ.Equation*, it must be re-implemented for trunk. Sergio will write his master thesis about this topic with the help of Jesus Escribano.
4. To make it possible to prove inequalities, another prover must be added. Judit Robu's dissertation explains a technique by using the AreaCAD method which is a construction of the area method (also implemented in ​GCLC) and the Cylindrical Algebra Decomposition. For this, we need an efficient CAD implementation. Currently ​QEPCAD seems to be the best option since it is written in pure C, and its only dependence, SACLIB is also written in pure C. However, SACLIB uses its internal Word data type which is both used for integers and pointers. Thus compiling SACLIB to Java may not be an easy task; maybe a SACLIB-like underlying library would be the solution for using QEPCAD inside GeoGebra. Another option is to use QEPCAD on server side as an outsourced web service for GeoGebra.

The prover (as a "clever machine") should choose the 2nd method if the thesis doesn't contain an inequality. Otherwise the 4th method should be used. If no result (or "unknown") is received, the 1st method should be used. This would be the first approach which can be changed later when we have experiences in real life problems and every day use. (The 3rd method will not be used currently, however it seems it is essentially the same as the 2nd method, without any simplifications.)

Plans personnel (as of 2012 Jan-March)

As decided by the GeoGebra Theorem Proving subproject committee (personnel: Tomas Recio, Markus Hohenwarter, Francisco Botana and Zoltan Kovacs), the following plans are settled:

• GeoGebra will have a main prover logic which can connect to several prover backends.
• By default, if there is no Internet connection, the OpenGeoProver subsystem will be used.
• If there is Internet connection, Botana's prover will be used by sending Gröbner basis calculations to the SingularWS subsystem. See ​Implementing theorem proving in GeoGebra by using a Singular webservice, Proceedings EACA 2012. Universidad de Alcala (2012) for details.
• As an experimental backend, Recio's prover can also be used. See ​Implementing theorem proving in GeoGebra by exact check of a statement in a bounded number of test cases, Proceedings EACA 2012. Universidad de Alcala (2012) for details
• The settings can be fine tuned in the Options/Settings menu in GeoGebra, so that a user could change the preferable backend.
• Prototypes for Botana's prover and Recio's prover will be demonstrated at EACA in Alcala de Henares, Spain, June 2012. Another (common) talk will also be given at CADGME in Novi Sad, Serbia, June 2012.
• The programming work will be done by Zoltan and Simon. Zoltan's work is mainly to implement Botana's prover, and Simon's is to work on Recio's prover (also as his master thesis at JKU, Linz).

In December 2011 Predrag and his PhD student, Ivan Petrovic also joined the team and offered contributions to plug OpenGeoProver in GeoGebra. We will present the ongoing work (and hopefully a prototype as well) in CADGME 2012. For plugging, the following changes should be done:

• Removing 3rd party libraries from OpenGeoProver
• Adding simplifyed XML export and prefixed expressions to GeoGebra

These steps will mostly be done by Ivan and Zoltan with the help of Simon. Some information can be read at Integrating OpenGeoProver.

The CAD related development is delayed to September 2012. (Hopefully, some (former) colleagues at RISC (Christopher Brown, Wolfgang Schreiner, Robert Vajda) could also help us in this.) Maybe SingularWS can be extended to provide a QEPCAD interface for CAD computations.

Related links and readings

• ​The main prover logic
• ​SingularWS and its ​GeoGebra interface

Some questions

• Think of the possible connection points of Sergio's locus line project as well.
• Plans with J.L. Valcarce's GDI software: Recognition of NDG polynomial output patterns. OpenGeoProver can also translate NDGs to geometrical statements.

Didactics

See the GeoGebra 2011 conference ​final result material for the "Reasoning and Proving" working group.

Mathematics: some investigation by using Gröbner basis

This section was originally the main part of this article, and should be put into another article. Since the first plans were about to use Gröbner basis in general, this part is quite detailed.

Problems with numerical calculations

As mentioned, GeoGebra can already answer a wide range of proving questions, but in some cases the answer will be unexact. Let's consider Miguel Abanades's example in the attached miguels_prover.ggb file. His construction contains the altitudes of a triangle and proofs that f is orthogonal to c by taking this expression and putting into g. Now when B is set to (40000,0), C is set to (30000,30000) and A is dragged in the neighborhood of the origin, g is changing randomly between true and false. However, this type of problem still could be solved by carefully chosen free points as comments 10 and 12 at #1044 suggest.

A natural answer to Miguel's problem that symbolic calculations should be used instead of numerical ones, which solves such questions in general. However, symbolic calculations may use more resources than numerical ones, including RAM, CPU and time. Transcendent (non-algebraic) problems may not be solved with symbolic methods. (E.g. "Show that sin(x) is always less than 2".)

Do we need to store the symbolic equation of an object?

For locus line equation GeoGebra currently constructs a graphical representation only in its current public versions. Sergio Arbeo already developed a prototype for adding the symbolic equation for locus equations as well - his development is available as a branch, and requires merging. His implementation creates equations for the dependent objects.

It is a natural idea to use Sergio's symbolic objects for theorem proving as well. However, there are even better ways for us. If we can use 3rd party libraries which can answer questions by not requiring symbolic input, then we can outsource such calculations for the appropriate library.

Possible non-numerical approaches

There are several non-numerical ways to be sure if a theorem is true. See Judit Robu's dissertation on this, for example. In short, the most promising methods are:

• Gröbner basis or Wu's method
• AreaCAD method (for inequalities)

They won't give the proofs, only an answer: generally yes, no, yes with some conditions.

Possibilities with Gröbner basis

Using Gröbner basis is a natural way in non-numerical approaches, since it is quite efficient. Sergio also uses a related technique in calculating the locus equations, and he uses the JAS subsystem for that (which has a built-in Gröbner basis support).

We will translate the statements into polynomial equations. To easily check if a statement is true when a set of premises are assumed, we can deny the statement and add to the premises. Iff the new set of premises gives contradiction, the theorem (i.e. the statement is a consequence of the premises) is true. Such a way of theorem proving can be calculated by computing the Gröbner basis of the polynomials of these new set of premises and getting the trivial ideal as result. This method was introduced by Kapur in 1986, however it is just a technical simplification of Kutzler and Stifter's method (1986). A quite detailed cookbook was published by Chou in 1988 on what to do for concrete problems.

Unfortunately, calculation of a Gröbner basis can be time consuming for some problems, especially if many equations or variables are given. To reduce the number of variables, for a 2 dimensional construction one can put a free point to the origin and a second one onto one of the axes. This method can save 3 variables, or yet a 4th one if we set the second point to (1,0). In 3 dimension the same technique can save 6 (or 7) variables.

It is important to know that Wu's method has the same computational difficulty like Gröbner basis has. Since Gröbner basis can be calculated by several mathematics software, here our checks are limited to that method, and we don't check the Wu implementations yet. (See also Predrag's experience with GCLC.)

Since we plan to use Gröbner basis calculations, we need to test if we can use a suitable Gröbner basis implementation for GeoGebra. Since GeoGebra is written in Java and the primary goal is to maintain the underlying subroutines inside of GeoGebra, the following ideas may help:

• Use JAS (the Java Algebra System) as a native Java underlying subsystem. It has built-in Gröbner basis calculations.
• Use Ted Kosan's MPReduce (based on JReduce, the Java port of Reduce). It has Gröbner basis calculations in the package groebner.

Gröbner implementations

JAS

JAS is intensively developed nowadays and its latest version has multi-thread and multi-core support. The newest version still can run on Java 1.5 and is significantly faster than the older versions.

We will refer to JAS1 and JAS2 as the two different versions. JAS1 is already a part of GeoGebra in Sergio Arbeo's branch for computing locus line equations.

MPReduce

MPReduce is the Java version of Reduce specially created for GeoGebra by Ted Kosan. Reduce is written in Lisp, and currently it supports 2 different Lisp implementations: CSL and PSL. CSL is the portable version, it requires less memory than PSL, but it can sometimes be slower at a maximum factor of 2.

GeoGebra is using the CSL based Lisp implementation for its CAS calculations when executing Reduce programs. Currently Reduce seems to behave significantly faster than MPReduce for certain problems, see #1572 for an example.

We will refer to Reduce/CSL, Reduce/PSL and MPReduce as the 3 different versions.

The tests

Here I provide JAS1, JAS2 and MPReduce source code. For reference Singular and Maxima code is also included (see below why). The original files (and their concept itself) were created by Erhard Aichinger (in Mathematica).

​Pappus

​Pappus's hexagon theorem states that given one set of collinear points A, B, C, and another set of collinear points C, D, E then the intersection points H, I, J of line pairs AE and DB, AF and DC, BF and EC are collinear.

To formulate this theorem into equations, first we require the following considerations:

1. A, B and C are collinear.
2. D, E and F are collinear.
3. A, H and E are collinear.
4. D, I and C are collinear.
5. A, I and F are collinear.
6. E, J and C are collinear.
7. B, J and F are collinear.

We also assume that

8. A, B and D are not collinear. (Collinearity would result (A=)H=I, so the statement of the theorem will be nonsense.)
9. A, B and E are not collinear. (Collinearity would result (B=)H=J, so the statement of the theorem will be nonsense.)

Our conclusion should be

10. H, I and J are collinear.

Instead of considering the theorem "(1-9) => (10)", we take the equivalent "(1-9), (10) is false => contradiction" system. In other words, we use reductio ad absurdum.

Now we need 2 technical details to uncover:

1. Collinearity can be checked with determinants. Points with coordinates (a,b), (c,d) and (e,f) are collinear iff det({{a,b,1},{c,d,1},{e,f,1}})=0.
2. Negation can be formulated by using the following theorem: f(x) does not equal 0 for some x iff z*f(x)=1 for some x and z constants.

This means we require 10 equations, but 3 of them will be negations.

Note that all program code below contain the unused variables g1 and g2.

GeoGebra

GeoGebra defines this construction as follows (simplified), the presentation related <element> tags are not shown:

1. <element type="point" label="A"/>
2. <element type="point" label="B"/>
3. command a=Line(A,B)
4. command C=Point(a)
5. <element type="point" label="D"/>
6. <element type="point" label="E"/>
7. command b=Line(D,E)
8. command F=Point(b)
9. command c=Line(A,E)
10. command d=Line(B,D)
11. command H=Intersect(d,c)
12. command e=Line(C,D)
13. command g=Line(C,E)
14. command h=Line(F,B)
15. command J=Intersect(h,g)
16. command f=Line(A,F)
17. command I=Intersect(f,e)
18. command i=Line(I,H)
19. command j=Line(I,J)
20. <expression label="k" exp="i ≟ j"/>

Note that to check if k is true, there is no need of implementing symbolic computations for GeoGebra. Instead, the following equations need to be set up:

• Patterns <element type="point" label="X"/> will introduce variables X1 and X2.
• Patterns like z=Line(X,Y) and Z=Point(z) will introduce variables Z1 and Z2 and set det({{X1,X2,1},{Y1,Y2,1},{Z1,Z2,1}}) as another polyinomial for the input of the Gröbner basis calculation. To be short, we can denote this determinant as DC(X1,X2,Y1,Y2,Z1,Z2) as well (determinant for collinearity).
• Patterns like c=Line(A,B), f=Line(D,E), G=Intersect(c,d) will introduce variables G1 and G2 and polynomials DC(A1,A2,B1,B2,G1,G2) and DC(D1,D2,E1,E2,G1,G2).
• The conclusion and the degeneration blocking polynomials are somewhat complicated to define. It is still a problem in GeoGebra to define the conclusion in a simple way.

Reduce

load groebner;
torder({a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2,g1,g2,h1,h2,i1,i2,j1,j2,z1,z2,z3},'revgradlex);
groebner({a1*(b2 - c2) + a2*( - b1 + c1) + b1*c2 - b2*c1,
d1*(e2 - f2) + d2*( - e1 + f1) + e1*f2 - e2*f1,
a1*( - e2 + h2) + a2*(e1 - h1) - e1*h2 + e2*h1,
b1*(d2 - h2) + b2*( - d1 + h1) + d1*h2 - d2*h1,
c1*(d2 - i2) + c2*( - d1 + i1)+ d1*i2 - d2*i1,
a1*( - f2 + i2) + a2*(f1 - i1) - f1*i2 + f2*i1,
c1*(e2 - j2) + c2*( - e1 + j1) + e1*j2 - e2*j1,
b1*( - f2 + j2) + b2*(f1 - j1) - f1*j2 + f2*j1,
a1*(b2*z2 - d2*z2)+ a2*( - b1*z2 + d1*z2) + b1*d2*z2 - b2*d1*z2 - 1,
a1*(b2*z3 - e2*z3) + a2*( - b1*z3 + e1*z3) + b1*e2*z3 - b2*e1*z3 - 1,
h1*(i2*z1 - j2*z1) + h2*( - i1*z1 + j1*z1) + i1*j2*z1 - i2*j1*z1 - 1});

JAS1

Use this for edu.jas.application.Examples:

    public static void example6() {
		String exam = "Rat(a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2,g1,g2,h1,h2,i1,i2,j1,j2,z1,z2,z3) L ( "
				+ "(a1*(b2 - c2) + a2*( - b1 + c1) + b1*c2 - b2*c1),"
				+ "(d1*(e2 - f2) + d2*( - e1 + f1) + e1*f2 - e2*f1),"
				+ "(a1*( - e2 + h2) + a2*(e1 - h1) - e1*h2 + e2*h1),"
				+ "(b1*(d2 - h2) + b2*( - d1 + h1) + d1*h2 - d2*h1),"
				+ "(c1*(d2 - i2) + c2*( - d1 + i1) + d1*i2 - d2*i1),"
				+ "(a1*( - f2 + i2) + a2*(f1 - i1) - f1*i2 + f2*i1),"
				+ "(c1*(e2 - j2) + c2*( - e1 + j1) + e1*j2 - e2*j1),"
				+ "(b1*( - f2 + j2) + b2*(f1 - j1) - f1*j2 + f2*j1),"
				+ "(a1*(b2*z2 - d2*z2) + a2*( - b1*z2 + d1*z2) + b1*d2*z2 - b2*d1*z2 - 1),"
				+ "(a1*(b2*z3 - e2*z3) + a2*( - b1*z3 + e1*z3) + b1*e2*z3 - b2*e1*z3 - 1),"
				+ "(h1*(i2*z1 - j2*z1) + h2*( - i1*z1 + j1*z1) + i1*j2*z1 - i2*j1*z1 - 1))";

		Reader source = new StringReader(exam);
		GenPolynomialTokenizer parser = new GenPolynomialTokenizer(source);
		PolynomialList<BigRational> F = null;
		List<GenPolynomial<BigRational>> G;
		try {
			F = (PolynomialList<BigRational>) parser.nextPolynomialSet();
		} catch (ClassCastException e) {
		} catch (IOException e) {
		}
		GroebnerBase<BigRational> bb = new GroebnerBaseSeq<BigRational>();
		G = bb.GB(F.list);
				PolynomialList<BigRational> t = new PolynomialList<BigRational>(F.ring,
				G);
		System.out.println("G = " + t);
	}

JAS2

    public static void example10() {
        String[] vars = { "a1", "a2", "b1", "b2", "c1", "c2", "d1", "d2", "e1", "e2", "f1", "f2", "g1", "g2",
    	    "h1", "h2", "i1", "i2", "j1", "j2", "z1", "z2", "z3" };

        BigRational br = new BigRational();
        GenPolynomialRing<BigRational> pring = new GenPolynomialRing<BigRational>(br, vars);

        GenPolynomial<BigRational> e1 = pring.parse("(a1*(b2 - c2) + a2*( - b1 + c1) + b1*c2 - b2*c1)");
        GenPolynomial<BigRational> e2 = pring.parse("(d1*(e2 - f2) + d2*( - e1 + f1) + e1*f2 - e2*f1)");
        GenPolynomial<BigRational> e3 = pring.parse("(a1*( - e2 + h2) + a2*(e1 - h1) - e1*h2 + e2*h1)");
        GenPolynomial<BigRational> e4 = pring.parse("(b1*(d2 - h2) + b2*( - d1 + h1) + d1*h2 - d2*h1)");
        GenPolynomial<BigRational> e5 = pring.parse("(c1*(d2 - i2) + c2*( - d1 + i1) + d1*i2 - d2*i1)");
        GenPolynomial<BigRational> e6 = pring.parse("(a1*( - f2 + i2) + a2*(f1 - i1) - f1*i2 + f2*i1)");
        GenPolynomial<BigRational> e7 = pring.parse("(c1*(e2 - j2) + c2*( - e1 + j1) + e1*j2 - e2*j1)");
        GenPolynomial<BigRational> e8 = pring.parse("(b1*( - f2 + j2) + b2*(f1 - j1) - f1*j2 + f2*j1)");
        GenPolynomial<BigRational> e9 = pring.parse("(a1*(b2*z2 - d2*z2) + a2*( - b1*z2 + d1*z2) + b1*d2*z2 - b2*d1*z2 - 1)");
        GenPolynomial<BigRational> e10 = pring.parse("(a1*(b2*z3 - e2*z3) + a2*( - b1*z3 + e1*z3) + b1*e2*z3 - b2*e1*z3 - 1)");
	GenPolynomial<BigRational> e11 = pring.parse("(h1*(i2*z1 - j2*z1) + h2*( - i1*z1 + j1*z1) + i1*j2*z1 - i2*j1*z1 - 1)");

        List<GenPolynomial<BigRational>> cp = new ArrayList<GenPolynomial<BigRational>>(11);
        cp.add(e1);
        cp.add(e2);
        cp.add(e3);
        cp.add(e4);
        cp.add(e5);
        cp.add(e6);
        cp.add(e7);
        cp.add(e8);
        cp.add(e9);
        cp.add(e10);
        cp.add(e11);

        List<GenPolynomial<BigRational>> gb;
        GroebnerBase<BigRational> sgb = GBFactory.getImplementation(br);
        gb = sgb.GB(cp);
        //System.out.println("gb = " + gb);

        PolynomialList<BigRational> pl = new PolynomialList<BigRational>(pring,gb);
        Ideal<BigRational> id = new Ideal<BigRational>(pl,true);
        System.out.println("cp = " + cp);
        System.out.println("id = " + id);

        Dimension dim = id.dimension();
        System.out.println("dim = " + dim);
    }

Singular

ring r=0,(a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2,g1,g2,h1,h2,i1,i2,j1,j2,z1,z2,z3),dp;
ideal I=a1*(b2 - c2) + a2*( - b1 + c1) + b1*c2 - b2*c1,
 d1*(e2 - f2) + d2*( - e1 + f1) + e1*f2 - e2*f1,
 a1*( - e2 + h2) + a2*(e1 - h1) - e1*h2 + e2*h1,
 b1*(d2 - h2) + b2*( - d1 + h1) + d1*h2 - d2*h1,
 c1*(d2 - i2) + c2*( - d1 + i1) + d1*i2 - d2*i1,
 a1*( - f2 + i2) + a2*(f1 - i1) - f1*i2 + f2*i1,
 c1*(e2 - j2) + c2*( - e1 + j1) + e1*j2 - e2*j1,
 b1*( - f2 + j2) + b2*(f1 - j1) - f1*j2 + f2*j1,
 a1*(b2*z2 - d2*z2)  + a2*( - b1*z2 + d1*z2) + b1*d2*z2 - b2*d1*z2 - 1,
 a1*(b2*z3 - e2*z3) + a2*( - b1*z3 +  e1*z3) + b1*e2*z3 - b2*e1*z3 - 1,
 h1*(i2*z1 - j2*z1) + h2*( - i1*z1 + j1*z1) + i1*j2*z1 - i2*j1*z1 - 1;
groebner(I);

Maxima

load(grobner);
poly_grobner([a1*(b2 - c2) + a2*( - b1 + c1) + b1*c2 - b2*c1,d1*(e2 - f2) + d2*( - e1 + f1)+
e1*f2 - e2*f1,a1*( - e2 + h2) + a2*(e1 - h1) - e1*h2 + e2*h1,b1*(d2 - h2) + b2*( - d1 + h1) +
d1*h2 - d2*h1,c1*(d2 - i2) + c2*( - d1 + i1)+ d1*i2 - d2*i1,a1*( - f2 + i2) + a2*(f1 - i1) -
f1*i2 + f2*i1,c1*(e2 - j2) + c2*( - e1 + j1) + e1*j2 - e2*j1,b1*( - f2 + j2) + b2*(f1 - j1)
- f1*j2 + f2*j1,a1*(b2*z2 - d2*z2)+ a2*( - b1*z2 + d1*z2) + b1*d2*z2 - b2*d1*z2 - 1,
a1*(b2*z3 - e2*z3) + a2*( - b1*z3 + e1*z3) + b1*e2*z3 - b2*e1*z3 - 1,h1*(i2*z1 - j2*z1)
+ h2*( - i1*z1 + j1*z1) + i1*j2*z1 - i2*j1*z1 - 1],
[a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2,g1,g2,h1,h2,i1,i2,j1,j2,z1,z2,z3]);

Pappus, reduced

The same as Pappus, but we assume that a1=a2=b1=0. We can do this without loss of generality.

We can even assume b2 to be a constant, for example 1, but for the tests we didn't use this reduction.

Thales

We assume that there is a circle with its center in the origin and 3 of its points are A(a,b), B(c,d) and P(x,y). The line lying on (a,b) and (x,y) is a diameter of the circle. We want to prove that AB is orthogonal to PB.

We require the following polynomials:

1. x²+y²-a²-b² (ensures x²+y²=a²+b², so the origin O is the same distance of P and A)
2. a²+b²-c²-d² (ensures a²+b²=c²+d², so OA=OB)
3. a+x
4. b+y (these two ones ensure that AB is a diameter)

Now the conclusion is (A-P)*(B-P)=0 (using vectors and scalar product), i.e. we need

5. ((x-c)*(a-c)+(y-d)*(b-d))*z-1

by applying the same method like for Pappus.

GeoGebra

GeoGebra defines the construction as follows:

1. command O=Intersect(xAxis,yAxis)
2. <element type="point" label="A"/>
3. command c=Circle(O,A)
4. command d=Line(A,O)
5. command C,B=Intersect(c,d)
6. command P=Point(c)
7. command b=Segment(A,P)
8. command a=Segment(P,B)
9. <expression label="s" exp="a ⊥ b" />

The altitudes of a triangle intersect each other at the orthocenter

Consider the ABC triangle with (a1,a2), (b1,b2), (c1,c2) points and D as its orthocenter with (d1,d2). Now assume:

1. AB ⊥ CD
2. AC ⊥ BD
3. A, B and C not collinear (we can omit this, however)

The conclusion is reductio ad absurdum:

4. BC ⊥ AD is not true

By using vectors and scalar product, we obtain the following polynomials:

1. (b1-a1)*(c1-d1)+(b2-a2)*(c2-d2)
2. (b1-d1)*(a1-c1)+(b2-d2)*(a2-c2)
3. z1*(b1*c2+a1*(b2-c2)-c1*b2-a2*(b1-c1))-1
4. z2*((a1-d1)*(b1-c1)+(a2-d2)*(b2-c2))-1

Each median of a triangle passes through the triangle's centroid

Consider the ABC triangle with (a1,a2), (b1,b2), (c1,c2) points, the midpoints of the sides D(d1,d2), E(e1,e2), F(f1,f2) and G as its centroid with (g1,g2). Now assume:

1. D is a midpoint of BC.
2. E is a midpoint of CA.
3. F is a midpoint of AB.
4. A, G, D are collinear.
5. B, G, E are collinear.

The conclusion is reductio ad absurdum:

6. C, G, F are not collinear.

By using vectors arithmetics and determinant we obtain these polynomials:

1. 2*d1-b1-c1, 2*d2-b2-c2
2. 2*e1-a1-c1, 2*e2-a2-c2
3. 2*f1-a1-b1, 2*f2-a2-b2
4. g1*d2+a1*(g2-d2)-d1*g2-a2*(g1-d1)
5. g1*e2+b1*(g2-e2)-e1*g2-b2*(g1-e1)
6. z*(g1*f2+c1*(g2-f2)-f1*g2-c2*(g1-f1))-1

The circumcenter of a triangle can be found as the intersection of any two of the three perpendicular bisectors

Consider the ABC triangle with (a1,a2), (b1,b2), (c1,c2) points, the midpoints of the sides D(d1,d2), E(e1,e2), F(f1,f2) and G as its circumcenter with (g1,g2). Now assume:

1. D is a midpoint of BC.
2. E is a midpoint of CA.
3. F is a midpoint of AB.
4. DG is orthogonal to BC.
5. EG is orthogonal to CA.

The conclusion is reductio ad absurdum:

6. FG is not orthogonal to AB.

By using vectors arithmetics and scalar products we obtain these polynomials:

1. 2*d1-b1-c1, 2*d2-b2-c2
2. 2*e1-a1-c1, 2*e2-a2-c2
3. 2*f1-a1-b1, 2*f2-a2-b2
4. (d1-g1)*(b1-c1)+(d2-g2)*(b2-c2)
5. (e1-g1)*(c1-a1)+(e2-g2)*(c2-a2)
6. z*((f1-g1)*(a1-b1)+(f2-g2)*(a2-b2))-1

Euler line

Consider the ABC triangle with (a1,a2), (b1,b2), (c1,c2) points, the midpoints of the sides D(d1,d2), E(e1,e2), F(f1,f2) and O(o1,o2) as its circumcenter , S(s1,s2) as its centroid and M(m1,m2) orthocenter. Now assume:

1. D is a midpoint of BC.
2. E is a midpoint of CA.
3. F is a midpoint of AB.
4. DO is orthogonal to BC.
5. EO is orthogonal to CA.
6. A, S, D are collinear.
7. B, S, E are collinear.
8. AM is orthogonal to BC.
9. BM is orthogonal to CA.
10. A, B, C are not collinear (non-degenerate case)

The conclusion is reductio ad absurdum:

11. O, S, M are not collinear.

The polynomials:

1. 2*d1-b1-c1, 2*d2-b2-c2
2. 2*e1-a1-c1, 2*e2-a2-c2
3. 2*f1-a1-b1, 2*f2-a2-b2
4. (d1-o1)*(b1-c1)+(d2-o2)*(b2-c2)
5. (e1-o1)*(c1-a1)+(e2-o2)*(c2-a2)
6. s1*d2+a1*(s2-d2)-d1*s2-a2*(s1-d1)
7. s1*e2+b1*(s2-e2)-e1*s2-b2*(s1-e1)
8. (a1-m1)*(b1-c1)+(a2-m2)*(b2-c2)
9. (b1-m1)*(c1-a1)+(b2-m2)*(c2-a2)
10. z1*(b1*c2+a1*(b2-c2)-c1*b2-a2*(b1-c1))-1
11. z2*(s1*m2+o1*(s2-m2)-m1*s2-o2*(s1-m1))-1

Simson line

Consider the ABC triangle with (a1,a2), (b1,b2), (c1,c2) points and P(p1,p2) lying on its circumcircle. Let D, E, F be the projection of P to BC, CA and AB, respectively. Let's assume the center of the circumcircle is in the origin O(0,0). Now:

1. OA=OB=OC=OP
2. PD ⊥ BC
3. B, C, D are collinear
4. PE ⊥ CA
5. C, A, E are collinear
6. PF ⊥ AB
7. A, B, F are collinear
8. ABC is non-degenerate

Conclusion is reductio ad absurdum:

9. D, E, F are not collinear.

In polynomials:

1. a1*a1+a2*a2-b1*b1-b2*b2, b1*b1+b2*b2-c1*c1-c2*c2, c1*c1+c2*c2-d1*d1-d2*d2, d1*d1+d2*d2-p1*p1-p2*p2
2. (p1-d1)*(b1-c1)+(p2-d2)*(b2-c2)
3. c1*d2+b1*(c2-d2)-d1*c2-b2*(c1-d1)
4. (p1-e1)*(c1-a1)+(p2-e2)*(c2-a2)
5. a1*e2+c1*(a2-e2)-e1*a2-c2*(a1-e1)
6. (p1-f1)*(a1-b1)+(p2-f2)*(a2-b2)
7. b1*f2+a1*(b2-f2)-f1*b2-a2*(b1-f1)
8. z1*(b1*c2+a1*(b2-c2)-c1*b2-a2*(b1-c1))-1
9. z2*(e1*f2+d1*(e2-f2)-f1*e2-d2*(e1-f1))-1

Simson line, reduced

Since Simson line test is slow (even for Singular), the point A could be put to (0,1). For this reason we add

10. a1, a2-1

Nine point circle

Consider the ABC triangle with (a1,a2), (b1,b2), (c1,c2) points, the midpoints of the sides D(d1,d2), E(e1,e2), F(f1,f2) and G(g1,g2) as the projection of A to BC. Let the center of the circle be in the origin. Now assume:

1. D is a midpoint of BC.
2. E is a midpoint of CA.
3. F is a midpoint of AB.
4. AG is orthogonal to BC.
5. B, C and G are collinear.
6. OD=OE=OF.
7. ABC is non-degenerate (A, B and C are not collinear).

Conclusion by reductio ad absurdum:

8. OF=OG is false.

By polinomials:

1. 2*d1-b1-c1, 2*d2-b2-c2
2. 2*e1-a1-c1, 2*e2-a2-c2
3. 2*f1-a1-b1, 2*f2-a2-b2
4. (a1-g1)*(b1-c1)+(a2-g2)*(b2-c2)
5. b1*c2+g1*(b2-c2)-c1*b2-g2*(b1-c1)
6. d1²+d2²-e1²-e2², f1²+f2²-e1²-e2²
7. z1*(b1*c2+a1*(b2-c2)-c1*b2-a2*(b1-c1))-1
8. z2*(g1²+g2²-e1²-e2²)-1

Angle bisector theorem

Let ABC a triangle and CD one of the angle bisectors of it. The theorem is simply that BD/AD=BC/AC. Unfortunately, formulating this for our technique is far not so simple. :-) But still possible!

Basically, length are to be written using their squares. This means the theorem itself is written to this form: BD²*AC²=BC²*AD². The square of length is calculated by Pythagoras, so the theorem will be described with the following polynomial (with no reductio ad absurdum yet):

((b1-c1)^2+(b2-c2)^2)*((a1-d1)^2+(a2-d2)^2)
-((a1-c1)^2+(a2-c2)^2)*((b1-d1)^2+(b2-d2)^2)

Another difficulty is to set an equation for the angle bisector. By using scalar product we can write BC*CD=|BC|*|CD|*cos(BCD) and AC*CD=-|AC|*|CD|*cos(BCD). Now we can obtain cos(BCD) from 2 equations, which means (BC*CD)²*|AC|²*|CD|²=(AC*CD)²*|BC|²*|CD|². This means we can use the following polynomial:

((b1-c1)*(c1-d1)+(b2-c2)*(c2-d2))^2*((a1-c1)^2+(a2-c2)^2)
-((a1-c1)*(c1-d1)+(a2-c2)*(c2-d2))^2*((b1-c1)^2+(b2-c2)^2)

We must also set collinearity for A, B and D and set non-degenerity for the ABC triangle. To sum up, we have the following polynomials:

1. b1*d2+a1*(b2-d2)-d1*b2-a2*(b1-d1) (collinearity),
2. ((b1-c1)*(c1-d1)+(b2-c2)*(c2-d2))²*((a1-c1)²+(a2-c2)²)-((a1-c1)*(c1-d1)+(a2-c2)*(c2-d2))²*((b1-c1)²+(b2-c2)²) (angle bisector),
3. z1*(b1*c2+a1*(b2-c2)-c1*b2-a2*(b1-c1))-1 (non-degenerity),
4. z2*(((b1-c1)²+(b2-c2)²)*((a1-d1)²+(a2-d2)²)-((a1-c1)²+(a2-c2)²)*((b1-d1)²+(b2-d2)²))-1 (conclusion reductio ad absurdum).

The results

The following table shows the timings for different tests and CAS. Measurement is in seconds. "-" means that the test was too slow: the tester had to stop computing without getting any results. "imm." means immediate answer, "n/a" means the test was not tried.

CAS (CPU) / Test	Pappus	Pappus, reduced	Thales	Altitudes
Mathematica (i7)	2.5	n/a	imm.	n/a
JAS1 (i5)	-	-	n/a	n/a
JAS2 (4xi5)	1.5	0.9	n/a	n/a
Reduce/PSL (i5)	130	0.95	n/a	n/a
Reduce/CSL (i7)	150	n/a	n/a	n/a
Reduce/CSL (i5)	n/a	1.05	n/a	n/a
GeoGebra (MPReduce)	-	-	imm.	n/a
Singular (i5)	0.20	0.19	imm.	n/a
Maxima (i5)	-	-	imm.*	imm.*

*Maxima forgot to remove the unnecessary polynomials from the final answer, poly_reduction() had to be called to force it. However, in this problem poly_reduction simply answerred the question.

More precise benchmarking on the GeoGebra test server

Here a 60 seconds of timeout is set. The more systems are benchmarked, the slower processes are to be expected. Measuring JAS2 is done by compiling the Java file first, so expect at least 3 seconds only for compilation (and other preparation). JAS2 ran on a single processor under Java 5.

CAS (CPU) / Test	​Pappus	​Pappus XX, reduced	​Thales	​Altitudes	​Centroid	​Circumcenter	​Euler line	​9 point circle	​Simson	​Simson, reduced	​Angle bisector
#vars	21	21	7	10	13	13	20	16	16	16	10
#polys	11	14	5	4	9	9	11	13	12	14	4
JAS2	55.99	29.30		3.46			12.15
Maxima	-	-	0.38	0.71	0.84	0.63	-	1.55	-	-	29.76
Reduce/PSL	-	-*	0.39	0.57	0.39	0.38	41.69	0.40	-	-	2.50
Singular	1.71	0.17	0.03	0.03	0.05	0.02	0.07	0.02	-	0.85	1.92

*Reduce/PSL has exited after 5.19 with memory allocation error.

XX We can even set b2 to 1 (or any constant) without loss of generality. ​Reduce/PSL finishes in 3.52, Singular in 1.59, JAS2 in 16.02, Maxima runs out of time.

Conclusion

If we don't use variable reduction, the only possible technology now is to use JAS2 (or Singular, but in praxis this is quite problematic - first we must compile its C++ code into Java by using e.g. ​Ephedra). Another option is to implement another algorithm for computing Gröbner basis for Reduce: certainly Faugere's F4/F5 algorithms may work (this is the preferred way, because it should be faster than JAS2).

By using variable reduction, Reduce/CSL could also be a solution. Unfortunately, MPReduce is slow for some unknown reason (#1572).

Problems on lack of resources

Even if omitting Gröbner basis calculations due to lack of resources, symbolic calculations may be required for some special problems. (Details to be written!) It is also possible to move the free points on non-algebraic curves and check if the statement is still true for at least N cases. If N is large enough, the statement must be true, but for mathematically correct calculations here we also require symbolic computing. (Zlatan Magajna does the same technique in his software ​OK Geometry, but without random free points and a large number of tests.)

The Overview section already has a suggestion on implementing a clever algorithm.