SigmaGeometry/rules.txt at main · TeamSigmaGeometry/SigmaGeometry · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
col A D C, col B E C, para A B D E, ?eqratio D C E C A D B E
cong A B D E, cong B C E F, eqangle A B C D E F, sameclock A B C D E F, ?contri1 A B C D E F
cong A B D E, cong B C E F, cong C A F D, sameclock A B C D E F ?contri1 A B C D E F
eqangle B A C F D E, eqangle C B A D E F, cong A B D E, ?contri2 A B C D E F
# eqangle B A C B D C, eqangle C B A D C B, ?simtri2 A B C D C B
eqangle A C B F E D, eqangle C B A D F E, ?simtri2 A B C D E F
perp A B B C, midp M A C, ?cong A M B M
para A B C D, cyclic A B C D, ?eqangle A D C D C B
midp M A B, perp O M A B, ?cong O A O B
# cong A M B M, cong A Q B Q, ?perp A B M Q
# cong A P B P, cong A Q B Q, cyclic A B P Q, ?perp P A A Q
cyclic A B C D, ?eqangle A B C A D C
cyclic A B C D, ?eqangle D A C D B C
eqangle A B C A D C, ?cyclic A B C D
eqangle C B A F E D, eqangle B A C E D F, sameclock A B C D E F, ?simtri1 A B C D E F
eqangle C B A F E D, eqangle B A C E D F, cong A C D F, sameclock A B C D E F, ?contri1 A B C D E F
eqangle B A C E D F, eqangle B C A D E F ?simtri2 A B C D E F
contri1 A B C D E F, ?eqangle A B C D E F
contri1 A B C D E F, ?cong A B D E
simtri1 A B C D E F, ?sameclock A B C D E F
contri2 A B C D E F, ?eqangle B A C E D F
eqangle B A C E D F, cong A B D F, cong A C D E, ?contri2 A B C D E F
simtri1 A B C D E F, ?eqangle A B C D E F
simtri2 A B C D E F, ?eqangle A C B F E D
contri2 A B C D E F, ?eqangle A C B F E D
simtri1 A B C D E F, ?eqratio A B A C D E D F
simtri2 A B C D E F ?eqratio A B D F B C E F
simtri2 A B C D E F ?eqratio A B D F A C D E
cyclic A B C D, circle O A B C, ?circle O A B D
# RHS congruence
perp A B B C, perp D E E F, cong A B D E, cong A C D F, sameclock A B C D E F, ?contri1 A B C D E F
perp A B B C, perp D F E F, cong A B D F, cong A C D E, ? contri2 A B C D E F
# The next rule will be removed once AR is able to derive intermediate rules and not just goals
# eqangle B A C E D F, eqangle A C B D F E, ?eqangle C B A F E D
# cyclic A B C D, cong O A O B, cong O A O C, eqangle B O A D O C, ?eqangle D A C B D A
eqangle C B A A D C, ?cong A C A C
 eqangle D B A C B D, ?cong B D B D
# Need to find a way to encode inscribed angles
cong O A O B, cong O A O C, col B O C, ?perp A B A C
eqangle A B C E F G, col B D C, ?eqangle A B D E F G
cong A M B M, col A M B, ?midp M A B
circle O A B C, perp O A A D, ?tchord O A B D
cong A B A C, ?eqangle C B A A C B
eqangle C B A A C B? cong A B A C
para A B D E, col A B C, ?para A C D E
circle O A B C, perp O A A D, ?eqangle B A D B C A
para A B A C, ?col A B C
cyclic A B C P, cyclic A B C Q, cyclic A B C R, eqangle A C B P R Q, ?cong A B P Q
eqangle P D F P D E, ? col D E F
col A D B, para D E B C, ?eqangle C B A E D A