GG B.1. - Modifications in sending input theorem from GG to OGP

[GoogleCodeExporter]

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.

Original issue reported on code.google.com by ivan.petrovic.matf on 14 Jun 2012 at 9:00

[GoogleCodeExporter]

Revisions r218 (main trunk), r219 (GeoGebra) and r220 (Area method) added 
modification to custom file reader to accept characters in UTF-8 format.

Original comment by ivan.petrovic.matf on 14 Jun 2012 at 9:50

[GoogleCodeExporter]

Revisions r221 (GeoGebra) and r222 (Area method) fixed conversion of GeoGebra 
theorems - correct converter will be used depending on prover method.

Revisions r223 (GeoGebra) and r224 (Area method) implemented parsing of theorem 
statements in infix notation alongside existing prefix notation.

Original comment by ivan.petrovic.matf on 14 Jun 2012 at 11:51

[GoogleCodeExporter]

New revisions r229 (GeoGebra) and r230 (Area method) fixed lots of bugs in 
input from GeoGebra to OGP and also bugs with some OGP constructions and 
statements.

Original comment by ivan.petrovic.matf on 16 Jun 2012 at 7:48

[GoogleCodeExporter]

Revision r231 is for main trunk - changes in OGP constructions and statements 
done in r229 are merged up to main development trunk.

Original comment by ivan.petrovic.matf on 16 Jun 2012 at 8:11

[GoogleCodeExporter]

Revisions r242 (GeoGebra) and r243 (Area method) added input parameter for 
output report format and added time of conversion to algebraic form to result 
value of prover execution time.

Original comment by ivan.petrovic.matf on 20 Jun 2012 at 8:58

[GoogleCodeExporter]

Revisions r246 (GeoGebra) and r247 (Area method) fixed reading of output prover 
results.

Original comment by ivan.petrovic.matf on 21 Jun 2012 at 8:21

[GoogleCodeExporter]

Previous title: GG A.2.; A.8. - Modifications in sending input theorem from GG 
to OGP
Remaining work is for stage B.1.

Original comment by ivan.petrovic.matf on 25 Jun 2012 at 6:30

• Changed title: GG B.1. - Modifications in sending input theorem from GG to OGP

[GoogleCodeExporter]

http://dev.geogebra.org/trac/changeset/18676 implements some kind of required 
behavior from GeoGebra side, but it is a question what is the desired output 
format. Currently GeoGebra sends the following XML part for the Prove command 
for the orthocenter6.ggb test:

<command name="Prove">
        <input a0="ArePerpendicular[Segment[B, C, poly1],Line[A, D]]"/>
        <output a0=""/>
</command>

instead of

<command name="Prove">
        <input a0="a ⊥ f"/>
        <output a0=""/>
</command>

We should reconsider of handling of the input theorem format in the GG -> OGP 
communication. By reverting http://dev.geogebra.org/trac/changeset/18676#file5, 
we can simply go back to the old behavior.

Similar outputs can be verified in 
ggb1.idm.jku.at/~kovzol/data/prover-20120713/tmp.zip (files 
.test.log-*.ggb-OpenGeoProver_Wu).

Original comment by kov...@gmail.com on 14 Jul 2012 at 4:56

[GoogleCodeExporter]

Latest fixes on GeoGebra side ([18999], [18996], [18991], [18989], [18986], 
[18979]) resolve this problem.

Now these are the Prove command parameters for the 
http://ggb1.idm.jku.at/~kovzol/data/prover-20120725/ output:

Ceva1.ggb;AreEqual[Segment[A, F] / Segment[F, B] Segment[B, D] / Segment[D, C] 
Segment[C, E] / Segment[E, A], 1]
Ceva2.ggb;AreEqual[Segment[A, G] / Segment[G, B] Segment[B, E] / Segment[E, C] 
Segment[C, F] / Segment[F, A],1]
Ceva3.ggb;AreEqual[Segment[A, G] / Segment[G, B] Segment[B, E] / Segment[E, C] 
Segment[C, F] / Segment[F, A],1]
Desargues.ggb;j
EulerLine.ggb;l
Pappus.ggb;AreCollinear[G, H, I]
Pythagoras.ggb;AreEqual[Segment[A, B]² + Segment[A, C]²,Segment[B, C]²]
Simson1.ggb;AreCollinear[E, F, G]
Simson2.ggb;AreCollinear[E, F, G]
Thales1.ggb;AreEqual[d,e]
Thales2.ggb;b
Thales3.ggb;ArePerpendicular[b,d]
Varignon.ggb;AreParallel[e, f]
bisector-midpoint.ggb;AreEqual[C, D]
centroid-median-ratio1.ggb;AreEqual[f,g]
centroid-median-ratio2.ggb;AreEqual[Segment[D, F] / Segment[F, A],1 / 2]
circumcenter1.ggb;h
circumcenter2.ggb;g
circumcenter3.ggb;AreConcurrent[d, e, f]
circumcenter4.ggb;AreConcurrent[h, i, j]
circumcenter5.ggb;AreEqual[e,f]
def-line-perpline-perpline.ggb;AreParallel[a, c]
def-points-on-a-circle1.ggb;AreConcyclic[B, C, D, E]
def-points-on-a-circle2.ggb;AreConcyclic[A, B, C, D]
def-points-on-a-line.ggb;AreCollinear[A, B, C]
foot-exists.ggb;f
line-circle-intersection.ggb;AreCollinear[A, E, B]
lines-parallel.ggb;AreParallel[a, b]
nine-points-circle.ggb;AreConcyclic[I, K, G, E]
orthocenter1.ggb;g
orthocenter2.ggb;g
orthocenter3.ggb;g
orthocenter4.ggb;g
orthocenter5.ggb;g
orthocenter6.ggb;ArePerpendicular[a,f]
orthocenter7.ggb;g
parallelogram-diagonals.ggb;AreEqual[E,F]
point-equal.ggb;AreEqual[A,A]
points-collinear.ggb;AreCollinear[A, B, C]
points-equal.ggb;AreEqual[A,B]
powerline-perpendicular.ggb;ArePerpendicular[a, b]
regular-triangle.ggb;AreEqual[b,d]
triangle-areas.ggb;AreEqual[Area[A, B, C],Area[A, B, D]]
triangle-medians.ggb;AreCollinear[B, G, E]
triangle-midsegment1.ggb;AreParallel[e, g]
triangle-midsegment2.ggb;e
triangle-midsegment3.ggb;AreParallel[c, d]
triangle-midsegment4.ggb;AreParallel[c, d]
triangle-midsegment5.ggb;AreParallel[b,d]

All outputs give a correct computation from OGP_WU (and also from OGP_AREA) for 
the 42 (41) well working examples.

Original comment by kov...@gmail.com on 25 Jul 2012 at 8:55

• Changed state: Fixed