Alphageometry seems not able to solve basic geometry question

[maokaiii]

Problem: Let ABC be a triangle. Let ∠A be 20°, ∠B be 110°, ∠C be 50°. Let BD be an altitude of the triangle ABC. Let AE be an angle bisector of triangle ABC. Let F be the intersection of BD and AE. Find ∠CFD.

Answer 60°

Translated problem: a b = segment a b; c = s_angle b a c -20, s_angle a b c 110; d = foot b a c; e = angle_bisector b a c; f = on_line f b d, on_line f a e; g = s_angle f c g 60, s_angle c f g -60 ? coll f d g

Alternate: a b = segment a b; c = s_angle b a c -20, s_angle a b c 110; d = foot b a c; e = angle_bisector b a c; f = on_line f b d, on_line f a e; g = s_angle f c g 60 ? eqangle f c f g f c f d

Setting:

BATCH_SIZE=8
BEAM_SIZE=16
DEPTH=2

And there is no solution

[maokaiii]

Or even this one:

a b c = iso_triangle a b c ? eqangle a b b c a c c b

[maokaiii]

Or even this one:

a b c = iso_triangle a b c ? eqangle a b b c a c c b

this seems to be the problem of directed angle, the order of side matters

a b c = iso_triangle a b c ? eqangle b a b c c b c a would work

[maokaiii]

Other problem, again there is a problem of directed angle a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c a c b

should be corrected as: a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c b c a

[XiaoYang66]

Hello, can you please tell me how do you know how to interpret the natural language into the language by dd+ar?

[maokaiii]

Just by reading IMO questions and compare it to imo txt file. Also read the nature paper (extended table 1 something like that) and def.txt

[XiaoYang66]

Ok, thank you very much. That help me a lot. Actually, I thought I might ignore some important file. But actually, the authors did not explain the detailed implementation just like the DD authors did(A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering)

I also find some simple question can not be solved by the DD+AR implementation, such as: a b c d = perp a b c d; e f = perp e f c d, ncoll a b e ? para a b e f or a b c = iso_triangle a b c ? eqdistance a b c a

[maokaiii]

I think it should be a b c = iso_triangle a b c ? cong a b a c eqdistance seems not a pure predicate so cannot be used as a goal.

[cutepiggy123]

Hi, can you help me to explain this one "g = s_angle f c g 60, s_angle c f g -60 ? coll f d g". G is a auxiliary point or something? What is coll? And can you use dd to solve it now? Thank you for your help!!

[XiaoYang66]

I think it should be a b c = iso_triangle a b c ? cong a b a c eqdistance seems not a pure predicate so cannot be used as a goal.

Hello, thank you very much, I replace eqdistance with the cong, it worked! That helps me a lot. I think the eqdistance may be related to the AR.

I am trying to figure all the rules out.

Some other scholars who are also interested with this repo have created a Google Sheets to document the rule in issue67

[XiaoYang66]

Hi, can you help me to explain this one "g = s_angle f c g 60, s_angle c f g -60 ? coll f d g". G is a auxiliary point or something? What is coll? And can you use dd to solve it now? Thank you for your help!!

Hello, I will try your question. If I figure it out, I will reply to you as soon as possible!

[XiaoYang66]

Hi, can you help me to explain this one "g = s_angle f c g 60, s_angle c f g -60 ? coll f d g". G is a auxiliary point or something? What is coll? And can you use dd to solve it now? Thank you for your help!!

Hello, for now, I can ensure the coll means that a list of points on the same line.

I think the define of coll belongs to DD part, which is implemented and explained by this paper

For other symbol in your problem, I am trying to figure them out.

[SarthakRoongta]

Hi, I am trying to get it to prove a triangle is an isosceles triangle knowing that two sides are equal. I tried "a b c = triangle, cong a b a c ? eqanagle b a b c c b c a" but it gives me a keyerror on "cong"

[maokaiii]

Hi, can you help me to explain this one "g = s_angle f c g 60, s_angle c f g -60 ? coll f d g". G is a auxiliary point or something? What is coll? And can you use dd to solve it now? Thank you for your help!!

here I am just constructing an equilateral triangle. Coll is collinear

[maokaiii]

Hi, I am trying to get it to prove a triangle is an isosceles triangle knowing that two sides are equal. I tried "a b c = triangle, cong a b a c ? eqanagle b a b c c b c a" but it gives me a keyerror on "cong"

I think that cong is used in goal only, which means you cannot make it before question mark

[Geomathart]

eqdistance is the command you need to use instead of cong in the construction.

[cutepiggy123]

Other problem, again there is a problem of directed angle a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c a c b

should be corrected as: a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c b c a

Is alphageometry possible to solve this after you correct this?

[Geomathart]

Yeah, alphageometry has no problem to solve the corrected version.

[maokaiii]

Other problem, again there is a problem of directed angle a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c a c b should be corrected as: a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c b c a

Is alphageometry possible to solve this after you correct this?

Of course, this much simpler problem is possible to be solved by alphageometry, which just use the fact of sum of internal angles of a triangle being 180 degree. (In fact can be solved in DDAR mode)

The main problem is in the very beginning.

[cutepiggy123]

Thanks guys!!! Do anyone know if alphageometry can use to find the length of a segment like find x, y of this example

[XiaoYang66]

hello, i find another problem that can not be solved by dd+ar or alphageometry a b c d = eq_trapezoid a b c d ? cong c a b d

[XiaoYang66]

hello, i find another problem that can not be solved by dd+ar or alphageometry a b c d = eq_trapezoid a b c d ? cong c a b d

I have found that the author has pointed that a similar problem taht can not be solved in line 452 in file jgex_file_ag_231.txt

[liyongjiang68]

Hello, may I ask if the code can solve the problem of line segment length and angle, and if similarity and congruence can be represented? Based on those 30 questions, I have derived some rules myself, but there are still too few. I hope someone can communicate these things together!

[tpgh24]

The current version of AG indeed has many limitations. I made some improvements in a fork repository and have some ideas to improve it, check out AG4Masses and issue 110

[ShChen233]

Other problem, again there is a problem of directed angle a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c a c b

should be corrected as: a b = segment a b; c = s_angle b a c -50, s_angle a b c 70; d = s_angle b a d 60 ? eqangle a b a d c b c a

however，the procedure is wrong