ivan-z-petrovic / open-geo-prover

Automatically exported from code.google.com/p/open-geo-prover [author of the original repository on GoogleCode]
3 stars 2 forks source link

GG B.1. - Modification of conversion of Intersection Point construction #23

Open GoogleCodeExporter opened 9 years ago

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

Original issue reported on code.google.com by ivan.petrovic.matf on 20 Jun 2012 at 12:30

GoogleCodeExporter commented 9 years ago
Revisions r239 (GeoGebra) and r240 (Area method) modified conversion of 
intersection point construction for algebraic provers.

Original comment by ivan.petrovic.matf on 20 Jun 2012 at 12:40

GoogleCodeExporter commented 9 years ago
Previous title: GG A.3. - Modification of conversion of Intersection Point 
construction
Remaining work is for stage B.1.

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