search

cmb33595 / open-geo-prover

Automatically exported from code.google.com/p/open-geo-prover
0 stars 0 forks source link

GG A.2. - Improvement of CP to disregard unnecessary constructions #14

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
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.

Original issue reported on code.google.com by ivan.petrovic.matf on 4 Jun 2012 at 11:49

GoogleCodeExporter commented 9 years ago 
Following revisions are made: r182 (main trunk), r183 (GeoGebra trunk) and r184 
(Area method baseline).

Original comment by ivan.petrovic.matf on 5 Jun 2012 at 12:44

GoogleCodeExporter commented 9 years ago

Original comment by ivan.petrovic.matf on 9 Jun 2012 at 11:35

GoogleCodeExporter commented 9 years ago 
New revision r204 (main trunk) fixed bugs in simplification of TP and in method 
that removes construction from TP. Change is in other branches (GeoGebra - r202 
and Area method - r203).

Original comment by ivan.petrovic.matf on 10 Jun 2012 at 7:41

GoogleCodeExporter commented 9 years ago 
There is new request for GeoGebra's branch of OGP:

 After conversion of GeoGebra constructions to OGP format and after simplification of construction list, it should be checked if partial objects (like segments, arcs, rays etc.) are used to construct a point on it (like in intersection command or in construction of foot etc.). Algebraic provers cannot deal with such problems since they cannot express the "between" relationship among points in polynomial form. In these cases prover should return an "undefined" result.

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

GoogleCodeExporter commented 9 years ago

Original comment by ivan.petrovic.matf on 17 Jun 2012 at 1:13