cmb33595 / open-geo-prover Goto Github PK

Currently OGP provides only construction of angle bisector for given angle.
However, it would be also useful to have a construction of congruent angle as 
well.

Steps to do:
1. Create new construction type: construction of second angle ray for given 
first ray, vertex and congruent angle. E.g. construct ray r=OB of angle <AOB 
for given points A and O and given angle <DEF which is congruent to <AOB (and 
with same orientation).
2. Create OGP XML Converter necessary for XML input of this type of 
construction.

Please see attached picture: it is example of construction for proving Euler's 
theorem - to construct point A from that example, OGP must provide the 
construction of congruent angle.

Construction Protocol has to be improved to remove all unnecessary 
constructions i.e. those constructions not required for theorem statement. That 
way input system of polynomials will be much simpler and therefore theorem 
proof will be faster.

This improvement has to be merged to GeoGebra dedicated trunk as well.

This issue document is for work to delete unnecessary directories and other 
resources from main development project.

GeoGebra commands for all types of reflections have been converted to OGP 
constructions. The same has to be done for other types of geometry 
transformations supported by GeoGebra:

1. rotations,
2. translations and
3. dilatations.

Current term "Construction Protocol" should be replaced by "Theorem Protocol" 
since it really contains information about entire theorem, not only about 
construction steps for the theorem.

Therefore, all related classes and packages have to be properly renamed.

OGP already has logging facility provided by Apache's log4j library which is 
compatible with GPL license.

However, it has to be replaced for GeoGebra's prover for two reasons:
1. GeoGebra needs only one .jar file of OGP and don't want to take other 3rd 
party libs in order to keep its .jar file as small as possible.
2. GeoGebra already has its own logger and wants to use the same in its prover.

To achieve this it is required:
1. firstly to examine existing GeoGebra logger;
2. then to implement logger interface in OGP on main development trunk and 
therefore provide the ability of easy replacement of logger implementations;
3. to download code for GeoGebra logger from GeoGebra source and put it into 
single logger implementation class that implements the OGP logger interface. 
This will be done only in OGP branch dedicated for GeoGebra.

Sub-stages of work where this issue belongs are:
A.2. and A.5.

It is necessary to implement API method for calling OGP prover from GeoGebra 
code.

The method should receive input prover parameters and the theorem 
(constructions and statement) in XML format and should return output results 
with NDG conditions list.

It is required to add QDParser (quick and dirty parser) for parsing XML files 
for input of geometry constructions. The same parser is used in GeoGebra code.

1. Take QDParser.java file from development trunk of GeoGebra and integrate in 
OGP's branch for GeoGebra.

2. Take DocHandler.java interface from GeoGebra's development trunk and 
integrate in OGP's branch for GeoGebra.

3. Implement custom document handler for purpose of parsing XML files with 
constructions imported from GeoGebra side (XML input will be in GeoGebra's XML 
format and only construction part will be present i.e. all between tags 
<construction> and </construction> including these 2 tags).

In attachment there is theorem whose proving fails with following error:

Exception in thread "main" java.lang.StackOverflowError
        at java.util.ArrayList.grow(ArrayList.java:242)
        at java.util.ArrayList.ensureExplicitCapacity(ArrayList.java:216)
        at java.util.ArrayList.ensureCapacityInternal(ArrayList.java:208)
        at java.util.ArrayList.add(ArrayList.java:440)
        at
com.ogprover.pp.tp.geoconstruction.PerpendicularLine.getInputLabels(Perpendicula
rLine.java:502)

1. Creation of new branch of OGP to be used within GeoGebra.

2. Cleanup of this new branch - removing unnecessary resources, adding new 
resources etc.

There is a bug when running help of OGP project from command line:

When user normally executes OGP from command line with some prover parameters, 
prover terminates normally and shows prompt line after execution. But when "-h" 
or "--help" is put instead of plain prover parameters of command line, in order 
to see prover help, the help contents is displayed but prompt line doesn't 
appear - it is misleading and looks like user has to insert something, but 
actually he has to type "Ctrl+C" to terminate the process.

Please provide normal process termination in case when project help is being 
displayed.

Code for Area Method is merged from OGP branch for GeoGebra up to main 
development trunk.

However, this method still cannot be tested and executed on main Dev trunk 
since input methods do not support Area Method. On GeoGebra branch, there are 
converters of GeoGebra input for algebraic and area methods and therefore Area 
method can be tested and executed there.

It is required to implement necessary changes on non-GeoGebra branches in order 
to provide conversion of input theorems to format suitable for Area Method in 
order to be able to use it.

It is necessary to implement the converter of geometry theorem statements from 
GeoGebra to OGP format.

Theorems are passed to OGP as strings in form "name[arg1, arg2, ..., argn]".
Later they could be passed in some other format and then new type of conversion 
would be required.

This issue is for initial implementation of parametric sets of points and one 
their version - conic sections.

1. First of all, implementation of Area Method will be merged from "OGP for 
GeoGebra with Area Method" branch down to base "OGP for GeoGebra" branch.
2. Next, special branch for Area Method will be deleted.
3. Then implementation of Area Method will be merged up to main development 
trunk of OGP.
4. Finally, implementation of Area Method will be merged down to other branches 
(at this moment it is only branch for Full Angle Method which is cut from main 
trunk).

NDG conditions will be represented in following way:

 "ndgCondName[arg1, arg2, ..., argn]"

e.g. "collinearPoints[A, B, C]".

This representation is general and more suitable for conversion to other 
formats (like textual representation, multilingual text representation, 
constructions of special cases of theorems etc).

For OGP internal use there will be a method for conversion of this 
representation to textual form.

For GeoGebra it will be enough just to send NDGs in this general format.

Unconverted NDGs from polynomial representation will be shown as polynomials. 
For this purpose it is required to implement method for printing of polynomials 
in ASCII character set without any special formatting e.g.:
   (2*u1^3 - 5*u1)*x3^4*x2*x1^5 - 4*x2*x1^4 + x2 = 0.

1. All third party libraries have to be reviewed to see if their licenses are 
GPL compatible.

2. Prompt message that appears on starting of OGP prover, when it is run from 
command line, must be updated to match GPL v3 license.

3. Corresponding disclaimer has to be added to all source code.

This issue is main place to submit all changes that fix small bugs found in OGP 
when it is run from GeoGebra prover. These small bugs are made in initial 
development covered by other issue documents, but they cover implementation 
tasks. So this is central place for all errors made in implementation of 
various parts of integration.

If any reported bug requires significant change or even reimplementation of 
some greater part of code that affects the logic of prover, then a separate 
issue has to be created to address that problem.

Steps to reproduce the problem:
1. Start project compilation from <dist> target of Ant build file.
2. Notice the output messages in Eclipse - there is no [junit] task executed.

Task [junit] should appear in log messages in Eclipse console when that task is 
executed. The issue is that it is not executed.

1. Creating new type of shortcut construction for list of simple constructions.
2. Fixing name of construction of reflected point.

This issue document is for initial implementation of support for solving 
RC-constructibility problems. These problems will be solved by algebraic method 
which uses simple triangulation algorithm (from Wu's method) to separate 
variables.

1. Ant build.xml file has to be improved to create minimal .jar file that will 
include only compiled classes, not additional resources like source code etc.

2. It is required to create a Linux shell script for compilation of OGP outside 
of Eclipse IDE.

It would be nice if we could get the NDG conditions back with the same objects 
as we send from GeoGebra.

Let's consider the following example:

...
d=Line[C,D]
e=Line[A,E]
...
h=ProveDetails[...]

Now we can get an NDG condition from OGP like this:

AreParallel[D,C,E,A]

But this is a little bit unelegant, and may be confusing for the GeoGebra 
users. Instead, it would be more beautiful to get AreParallel[e,d], or even
better if the parameters would be alphabetically ordered (AreParallel[d,e]).

Documentation of OGP has to contain several examples of theorems proved with 
simple Wu's method. Input is in OGP's internal XML format, while output is 
generated TeX report translated to PDF.

Following constructions should be added to OGP:

1. Construction of angle of 60 degrees;
2. "Construction" of angle's trisector;
3. Construction of triple angle;
4. Construction of third addend for two given angles to angle of 60 degrees.

Also following theorem statements should be added:

1. Equilateral triangle;
2. Angle of specified size (e.g. 60 degrees);
3. Linear combination of squares of segments' lengths.

These constructions and statements are necessary to be able to prove several 
well known geometry theorems, like Morley's theorem.

   Construction of tangent line from given point to given circle/conic should implicitly construct a touch point of that line and specified circle/conic. Currently this is not the case and therefore conversion of construction protocol to algebraic form may fail assuming this point is implicitly constructed.
   Workaround for this issue is to explicitly add construction of this touch point.

Example:
   These construction steps will fail to convert to polynomial form:

   <pfree label="$A$" />
   <pfree label="$H_{a}$" />
   <pfree label="$I$" />
   <ltwopts label ="$h_{a}$" point1="$A$" point2="$H_{a}$" />
   <lperp label ="$a$" point="$H_{a}$" baseline="$h_{a}$" />
   <pfoot label ="$P_{\_G14517}$" origpt="$I$" baseline="$a$" />
   <ccenterpt label ="$k(I,P_{a})$" center="$I$" point="$P_{\_G14517}$" />
   <ltangent label ="$c$" basept="$A$" pointset="$k(I,P_{a})$" />
   <ltangent label ="$b$" basept="$A$" pointset="$k(I,P_{a})$" />
   <pintersect label ="$B$" set1="$c$" set2="$a$" />
   <pintersect label ="$C$" set1="$a$" set2="$b$" />

   In these steps, there is tangent line c which by construction has only one point A, the point from which it has been constructed as a tangent to circle k. We assume it also has a touch point with circle k but that point currently is not implicitly constructed in OGP and that is an issue. Similarly, tangent line b has only one point A explicitly constructed. Then in last construction steps, points B and C are constructed as intersection points of line a and one of these tangents (b and c respectively). But, to transform these steps to polynomial form, each of two lines that intersect each other have to have at least 2 points, which is not the case since both b and c have just 1 point each.
   Workaround for this is to explicitly add touch point (in construction sample below they are marked with comments "add 1" and "add 2" before each of them):
   <pfree label="$A$" />
   <pfree label="$H_{a}$" />
   <pfree label="$I$" />
   <ltwopts label ="$h_{a}$" point1="$A$" point2="$H_{a}$" />
   <lperp label ="$a$" point="$H_{a}$" baseline="$h_{a}$" />
   <pfoot label ="$P_{\_G14517}$" origpt="$I$" baseline="$a$" />
   <ccenterpt label ="$k(I,P_{a})$" center="$I$" point="$P_{\_G14517}$" />
   <ltangent label ="$c$" basept="$A$" pointset="$k(I,P_{a})$" />
   <!-- add 1 -->
   <pintersect label ="$C1$" set1="$c$" set2="$k(I,P_{a})$" />
   <ltangent label ="$b$" basept="$A$" pointset="$k(I,P_{a})$" />
   <!-- add 2 -->
   <pintersect label ="$B1$" set1="$b$" set2="$k(I,P_{a})$" />
   <pintersect label ="$B$" set1="$c$" set2="$a$" />
   <pintersect label ="$C$" set1="$a$" set2="$b$" />

This issue is about implementation of usage of log file whose destination 
(path) and name are set by user.

If there are multiple Prove (or ProveDetails) commands in the XML given, then 
GeoGebra should communicate which one to be proven by OpenGeoProver.

Maybe it would be a good solution to pass the name of the object as well. E.g. a

h=ProveDetails[AreEqual[C,D]]

could be selected by sending the object "h" to OGP.

1. XML of GeoGebra could have Prove command with input which is statement 
command in infix notations that uses Unicode characters in UTF-8 format. They 
are mainly used to express equality. Modify XML parsing of Prove command to 
cover these cases.

2. New input parameters (like format of OGP report, path of log file etc.) have 
to be defined for usage of OGP from GeoGebra.

GeoGebra command for intersection point can return more then one point (e.g. 
intersections of two circles or of a circle and a line return 2 points each, 
while intersection of two ellipses return 4 points in total).

Prover cannot distinguish between 2 intersection points if they are both 
constructed in same way - to satisfy condition that belong to each of two point 
sets. Instead of that, only one can be constructed this way, and another is 
constructed differently:

1. If line intersects a circle, first construct foot of circle center to given 
line and then construct central symmetric point of first intersection point 
w.r.t. foot point.

2. If two circles intersect each other, reflect first intersection point about 
central line (line which connects centers of given circles).

There are also issues when new intersection points are constructed (so with new 
labels) but some of previous constructed points satisfy condition for 
intersection point. In that case some of new points has to be renamed by label 
of old point. GeoGebra offers coordinates of constructed points in its XML and 
this can be used to compare points (when they are same but with different 
labels). That way we can know what old point to use to rename new intersection 
point. But this work is scheduled for next stage/phase of integration 
development.