All Rules

Rules allow the engine to create new facts given that a list of other facts is true. They correspond to mathematical theorems.

The basic language of geometrical facts are the predicates with their arguments.

Each rule is a constant instance of newclid.rule.Rule.

For example in:

R00_PERPENDICULARS_GIVE_PARALLEL = Rule(

id=”r00”, description=”Perpendiculars give parallel”, premises_txt=(“perp A B C D”, “perp C D E F”, “ncoll A B E”), conclusions_txt=(“para A B E F”,),

)

The id being between r00-r42 means it was one of the rules used in the original AlphaGeometry.

“perp”, “ncoll”, and “para” are predicates defining geoemtric relations between geometric objects.

A, B, C, D, E, F are points used in the rule. Because the rule doesn’t have an allow_point_repetition argument, each point will be considered unique for the rule application.

This file contains all the rules created through the development of Newclid.

The rules currently in use are the ones in the list DEFAULT_RULES below.

DEFAULT_RULES: set[Rule] = {Rule(id='r03', description='Arc determines internal angles', premises_txt=('cyclic A B P Q',), conclusions_txt=('eqangle P A P B Q A Q B', 'eqangle A Q A P B Q B P', 'eqangle A B B Q A P P Q', 'eqangle A B A P Q B Q P'), allow_point_repetition=False), Rule(id='r04', description='Congruent angles are in a cyclic', premises_txt=('eqangle P A P B Q A Q B', 'ncoll P Q A B'), conclusions_txt=('cyclic A B P Q',), allow_point_repetition=False), Rule(id='r07', description='Thales Theorem I', premises_txt=('para A B C D', 'coll O A C', 'coll O B D', 'ncoll O A B'), conclusions_txt=('simtri O A B O C D', 'eqratio O A C A O B B D', 'eqratio O C A C O D B D'), allow_point_repetition=False), Rule(id='r11', description='Bisector theorem I', premises_txt=('eqratio D B D C A B A C', 'coll D B C', 'ncoll A B C'), conclusions_txt=('eqangle A B A D A D A C',), allow_point_repetition=False), Rule(id='r12', description='Bisector theorem II', premises_txt=('eqangle A B A D A D A C', 'coll D B C', 'ncoll A B C'), conclusions_txt=('eqratio D B D C A B A C',), allow_point_repetition=False), Rule(id='r19', description='Hypotenuse is diameter', premises_txt=('perp A B B C', 'midp M A C'), conclusions_txt=('cong A M B M',), allow_point_repetition=False), Rule(id='r20', description='Diameter is hypotenuse', premises_txt=('circle O A B C', 'coll O A C'), conclusions_txt=('perp A B B C',), allow_point_repetition=False), Rule(id='r25', description='Diagonals of parallelogram I', premises_txt=('midp M A B', 'midp M C D'), conclusions_txt=('para A C B D',), allow_point_repetition=False), Rule(id='r26', description='Diagonals of parallelogram II', premises_txt=('midp M A B', 'para A C B D', 'para A D B C', 'ncoll A B C'), conclusions_txt=('midp M C D',), allow_point_repetition=False), Rule(id='r27', description='Thales theorem II', premises_txt=('eqratio O A A C O B B D', 'coll O A C', 'coll O B D', 'ncoll A B C', 'sameside A O C B O D'), conclusions_txt=('para A B C D',), allow_point_repetition=False), Rule(id='r28', description='Overlapping parallels', premises_txt=('para A B A C',), conclusions_txt=('coll A B C',), allow_point_repetition=False), Rule(id='r34', description='AA Similarity of triangles (Direct)', premises_txt=('eqangle B A B C Q P Q R', 'eqangle C A C B R P R Q', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtri A B C P Q R',), allow_point_repetition=True), Rule(id='r35', description='AA Similarity of triangles (Reverse)', premises_txt=('eqangle B A B C Q R Q P', 'eqangle C A C B R Q R P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtrir A B C P Q R',), allow_point_repetition=True), Rule(id='r36', description='ASA Congruence of triangles (Direct)', premises_txt=('eqangle B A B C Q P Q R', 'eqangle C A C B R P R Q', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r37', description='ASA Congruence of triangles (Reverse)', premises_txt=('eqangle B A B C Q R Q P', 'eqangle C A C B R Q R P', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r41', description='Thales theorem III', premises_txt=('para A B C D', 'coll M A D', 'coll N B C', 'eqratio M A M D N B N C', 'sameside M A D N B C'), conclusions_txt=('para M N A B',), allow_point_repetition=False), Rule(id='r42', description='Thales theorem IV', premises_txt=('para A B C D', 'coll M A D', 'coll N B C', 'para M N A B', 'ncoll A B C'), conclusions_txt=('eqratio M A M D N B N C',), allow_point_repetition=False), Rule(id='r43', description='Orthocenter theorem', premises_txt=('perp A B C D', 'perp A C B D', 'ncoll A B C'), conclusions_txt=('perp A D B C',), allow_point_repetition=False), Rule(id='r44', description="Pappus's theorem", premises_txt=('coll A B C', 'coll P Q R', 'coll X A Q', 'coll X P B', 'coll Y A R', 'coll Y P C', 'coll Z B R', 'coll Z C Q'), conclusions_txt=('coll X Y Z',), allow_point_repetition=False), Rule(id='r46', description='Incenter theorem', premises_txt=('eqangle A B A X A X A C', 'eqangle B A B X B X B C', 'ncoll A B C'), conclusions_txt=('eqangle C B C X C X C A',), allow_point_repetition=False), Rule(id='r49', description='Recognize center of circle (cyclic)', premises_txt=('circle O A B C', 'cyclic A B C D'), conclusions_txt=('cong O A O D',), allow_point_repetition=False), Rule(id='r50', description='Recognize center of cyclic (cong)', premises_txt=('cyclic A B C D', 'cong O A O B', 'cong O C O D', 'npara A B C D'), conclusions_txt=('cong O A O C',), allow_point_repetition=False), Rule(id='r51', description='Midpoint splits in two', premises_txt=('midp M A B',), conclusions_txt=('rconst M A A B 1/2',), allow_point_repetition=False), Rule(id='r52', description='Properties of similar triangles (Direct)', premises_txt=('simtri A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('eqangle B A B C Q P Q R', 'eqangle A B A C P Q P R', 'eqangle A C B C P R Q R', 'eqratio B A B C Q P Q R', 'eqratio B C A C Q R P R'), allow_point_repetition=True), Rule(id='r53', description='Properties of similar triangles (Reverse)', premises_txt=('simtrir A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('eqangle B A B C Q R Q P', 'eqangle A B A C P R P Q', 'eqangle A C B C Q R P R', 'eqratio B A B C Q P Q R', 'eqratio B C A C Q R P R'), allow_point_repetition=True), Rule(id='r54', description='Definition of midpoint', premises_txt=('cong M A M B', 'coll M A B'), conclusions_txt=('midp M A B',), allow_point_repetition=False), Rule(id='r56', description='Properties of midpoint (coll)', premises_txt=('midp M A B',), conclusions_txt=('coll M A B',), allow_point_repetition=False), Rule(id='r58', description='Same chord same arc I', premises_txt=('cyclic A B C P Q R', 'cong A B P Q', 'nperp A C B C', 'sameclock C A B R P Q', 'sameside C A B R P Q'), conclusions_txt=('eqangle C A C B R P R Q',), allow_point_repetition=False), Rule(id='r59', description='Same chord same arc II', premises_txt=('cyclic A B C P Q R', 'cong A B P Q', 'nperp A C B C', 'sameclock C B A R P Q', 'nsameside C B A R P Q'), conclusions_txt=('eqangle C A C B R P R Q',), allow_point_repetition=False), Rule(id='r60', description='SSS Similarity of triangles (Direct)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtri A B C P Q R',), allow_point_repetition=True), Rule(id='r61', description='SSS Similarity of triangles (Reverse)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtrir A B C P Q R',), allow_point_repetition=True), Rule(id='r62', description='SAS Similarity of triangles (Direct)', premises_txt=('eqratio B A B C Q P Q R', 'eqangle B A B C Q P Q R', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtri A B C P Q R',), allow_point_repetition=True), Rule(id='r63', description='SAS Similarity of triangles (Reverse)', premises_txt=('eqratio B A B C Q P Q R', 'eqangle B A B C Q R Q P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtrir A B C P Q R',), allow_point_repetition=True), Rule(id='r64', description='SSS Congruence of triangles (Direct)', premises_txt=('cong A B P Q', 'cong B C Q R', 'cong C A R P', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r65', description='SSS Congruence of triangles (Reverse)', premises_txt=('cong A B P Q', 'cong B C Q R', 'cong C A R P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r66', description='SAS Congruence of triangles (Direct)', premises_txt=('cong A B P Q', 'cong B C Q R', 'eqangle B A B C Q P Q R', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r67', description='SAS Congruence of triangles (Reverse)', premises_txt=('cong A B P Q', 'cong B C Q R', 'eqangle B A B C Q R Q P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r68', description='Similarity without scaling (Direct)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r69', description='Similarity without scaling (Reverse)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r70', description='Projective harmonic conjugate', premises_txt=('coll A L M', 'coll A K N', 'coll B K M', 'coll B L N', 'coll C M N', 'coll D K L', 'coll A B C D'), conclusions_txt=('eqratio A C A D B C B D',), allow_point_repetition=False), Rule(id='r71', description='Resolution of ratios', premises_txt=('eqratio A B A C D E D F', 'coll A B C', 'coll D E F', 'sameside A B C D E F'), conclusions_txt=('eqratio A B B C D E E F',), allow_point_repetition=False), Rule(id='r74', description='Intersection of angle bisector and perpendicular bisector', premises_txt=('eqangle C A C D C D C B', 'cong D A D B', 'ncoll A B C D', 'nperp A B C D'), conclusions_txt=('cyclic A B C D',), allow_point_repetition=False), Rule(id='r77', description='Properties of congruent triangles (Direct)', premises_txt=('contri A B C P Q R',), conclusions_txt=('simtri A B C P Q R', 'cong A B P Q'), allow_point_repetition=True), Rule(id='r78', description='Properties of congruent triangles (Reverse)', premises_txt=('contrir A B C P Q R',), conclusions_txt=('simtrir A B C P Q R', 'cong A B P Q'), allow_point_repetition=True), Rule(id='r79', description='Divide congruence equation by segment', premises_txt=('cong A B C D', 'diff X Y', 'diff A B', 'diff C D'), conclusions_txt=('eqratio A B X Y C D X Y',), allow_point_repetition=True), Rule(id='r80', description='Same chord same arc III', premises_txt=('cyclic A B P Q', 'cong A B P Q', 'npara A P B Q'), conclusions_txt=('eqangle P A P B P B Q B',), allow_point_repetition=False), Rule(id='r81', description='Same chord same arc IV', premises_txt=('cyclic A B P Q', 'cong A B P Q', 'sameclock A P B A P Q'), conclusions_txt=('eqangle P A P B Q B P B',), allow_point_repetition=False), Rule(id='r82', description='Parallel from collinear', premises_txt=('coll A B C',), conclusions_txt=('para A B B C', 'para A B A C'), allow_point_repetition=False), Rule(id='r83', description='Betweeness condition I', premises_txt=('coll A B C', 'obtuse_angle A B C'), conclusions_txt=('lequation 1/1 A B 1/1 B C -1/1 A C 0',), allow_point_repetition=False), Rule(id='r84', description='Betweeness condition II', premises_txt=('lequation 1/1 A B 1/1 B C -1/1 A C 0',), conclusions_txt=('coll A B C',), allow_point_repetition=False), Rule(id='r85', description='Generalized Pythagorean theorem I', premises_txt=('perp A B C D',), conclusions_txt=('lequation 1/1 A C * A C 1/1 B D * B D -1/1 A D * A D -1/1 B C * B C 0',), allow_point_repetition=False), Rule(id='r86', description='Generalized Pythagorean theorem II', premises_txt=('lequation 1/1 A C * A C 1/1 B D * B D -1/1 A D * A D -1/1 B C * B C 0', 'ncoll A B C'), conclusions_txt=('perp A B C D',), allow_point_repetition=False), Rule(id='r87', description='Characterization of circumcenter I', premises_txt=('cong O A O C', 'aequation 1/1 A B B C 1/1 C A A O 90o'), conclusions_txt=('circle O A B C',), allow_point_repetition=False), Rule(id='r88', description='Characterization of circumcenter II', premises_txt=('circle O A B C',), conclusions_txt=('aequation 1/1 A B B C 1/1 C A A O 90o',), allow_point_repetition=False), Rule(id='r89', description='Length of a median of a triangle', premises_txt=('midp M A B', 'ncoll A B C'), conclusions_txt=('lequation 2/1 A M * A M -2/1 B C * B C -2/1 A C * A C 1/1 A B * A B 0',), allow_point_repetition=False), Rule(id='r90', description='Parallelogram law', premises_txt=('para A B C D', 'para A D B C', 'ncoll A B C'), conclusions_txt=('lequation 2/1 A B * A B 2/1 B C * B C -1/1 A C * A C -1/1 B D * B D 0',), allow_point_repetition=False), Rule(id='r91', description='Equal angles in an isosceles trapezoid', premises_txt=('cong A B C D', 'para A D B C', 'npara A B C D'), conclusions_txt=('eqangle C A C B B C B D',), allow_point_repetition=False), Rule(id='r92', description='Any diameter of a circle crosses the center', premises_txt=('midp O A B', 'circle O A B C', 'cyclic A B C D', 'cong A B C D'), conclusions_txt=('coll O C D',), allow_point_repetition=False)}

The rules effectively used on a normal run of the engine.

ALL_RULES: list[Rule] = [Rule(id='r00', description='Perpendiculars give parallel', premises_txt=('perp A B C D', 'perp C D E F', 'ncoll A B E'), conclusions_txt=('para A B E F',), allow_point_repetition=False), Rule(id='r01', description='Definition of cyclic', premises_txt=('cong O A O B', 'cong O B O C', 'cong O C O D'), conclusions_txt=('cyclic A B C D',), allow_point_repetition=False), Rule(id='r02', description='Parallel from inclination', premises_txt=('eqangle A B P Q C D P Q',), conclusions_txt=('para A B C D',), allow_point_repetition=False), Rule(id='r03', description='Arc determines internal angles', premises_txt=('cyclic A B P Q',), conclusions_txt=('eqangle P A P B Q A Q B', 'eqangle A Q A P B Q B P', 'eqangle A B B Q A P P Q', 'eqangle A B A P Q B Q P'), allow_point_repetition=False), Rule(id='r04', description='Congruent angles are in a cyclic', premises_txt=('eqangle P A P B Q A Q B', 'ncoll P Q A B'), conclusions_txt=('cyclic A B P Q',), allow_point_repetition=False), Rule(id='r05', description='Same arc same chord', premises_txt=('cyclic A B C P Q R', 'eqangle C A C B R P R Q'), conclusions_txt=('cong A B P Q',), allow_point_repetition=False), Rule(id='r06', description='Base of half triangle', premises_txt=('midp E A B', 'midp F A C'), conclusions_txt=('para E F B C',), allow_point_repetition=False), Rule(id='r07', description='Thales Theorem I', premises_txt=('para A B C D', 'coll O A C', 'coll O B D', 'ncoll O A B'), conclusions_txt=('simtri O A B O C D', 'eqratio O A C A O B B D', 'eqratio O C A C O D B D'), allow_point_repetition=False), Rule(id='r08', description='Right triangles common angle I', premises_txt=('perp A B C D', 'perp E F G H', 'npara A B E F'), conclusions_txt=('eqangle A B E F C D G H',), allow_point_repetition=False), Rule(id='r09', description='Sum of angles of a triangle', premises_txt=('eqangle A B C D M N P Q', 'eqangle C D E F P Q R U', 'npara A B E F'), conclusions_txt=('eqangle A B E F M N R U',), allow_point_repetition=False), Rule(id='r10', description='Ratio cancellation', premises_txt=('eqratio A B C D M N P Q', 'eqratio C D E F P Q R U'), conclusions_txt=('eqratio A B E F M N R U',), allow_point_repetition=False), Rule(id='r11', description='Bisector theorem I', premises_txt=('eqratio D B D C A B A C', 'coll D B C', 'ncoll A B C'), conclusions_txt=('eqangle A B A D A D A C',), allow_point_repetition=False), Rule(id='r12', description='Bisector theorem II', premises_txt=('eqangle A B A D A D A C', 'coll D B C', 'ncoll A B C'), conclusions_txt=('eqratio D B D C A B A C',), allow_point_repetition=False), Rule(id='r13', description='Isosceles triangle equal angles', premises_txt=('cong O A O B', 'ncoll O A B'), conclusions_txt=('eqangle O A A B A B O B',), allow_point_repetition=False), Rule(id='r14', description='Equal base angles imply isosceles', premises_txt=('eqangle A O A B B A B O', 'ncoll O A B'), conclusions_txt=('cong O A O B',), allow_point_repetition=False), Rule(id='r15', description='Arc determines inscribed angles (tangent)', premises_txt=('circle O A B C', 'perp O A A X'), conclusions_txt=('eqangle A X A B C A C B',), allow_point_repetition=False), Rule(id='r16', description='Same arc giving tangent', premises_txt=('circle O A B C', 'eqangle A X A B C A C B'), conclusions_txt=('perp O A A X',), allow_point_repetition=False), Rule(id='r17', description='Central angle vs inscribed angle I', premises_txt=('circle O A B C', 'midp M B C'), conclusions_txt=('eqangle A B A C O B O M',), allow_point_repetition=False), Rule(id='r18', description='Central angle vs inscribed angle II', premises_txt=('circle O A B C', 'coll M B C', 'eqangle A B A C O B O M'), conclusions_txt=('midp M B C',), allow_point_repetition=False), Rule(id='r19', description='Hypotenuse is diameter', premises_txt=('perp A B B C', 'midp M A C'), conclusions_txt=('cong A M B M',), allow_point_repetition=False), Rule(id='r20', description='Diameter is hypotenuse', premises_txt=('circle O A B C', 'coll O A C'), conclusions_txt=('perp A B B C',), allow_point_repetition=False), Rule(id='r21', description='Cyclic trapezoid', premises_txt=('cyclic A B C D', 'para A B C D'), conclusions_txt=('eqangle A D C D C D C B',), allow_point_repetition=False), Rule(id='r22', description='Bisector construction', premises_txt=('midp M A B', 'perp O M A B'), conclusions_txt=('cong O A O B',), allow_point_repetition=False), Rule(id='r23', description='Bisector is perpendicular', premises_txt=('cong A P B P', 'cong A Q B Q'), conclusions_txt=('perp A B P Q',), allow_point_repetition=False), Rule(id='r24', description='Cyclic kite', premises_txt=('cong A P B P', 'cong A Q B Q', 'cyclic A B P Q'), conclusions_txt=('perp P A A Q',), allow_point_repetition=False), Rule(id='r25', description='Diagonals of parallelogram I', premises_txt=('midp M A B', 'midp M C D'), conclusions_txt=('para A C B D',), allow_point_repetition=False), Rule(id='r26', description='Diagonals of parallelogram II', premises_txt=('midp M A B', 'para A C B D', 'para A D B C', 'ncoll A B C'), conclusions_txt=('midp M C D',), allow_point_repetition=False), Rule(id='r27', description='Thales theorem II', premises_txt=('eqratio O A A C O B B D', 'coll O A C', 'coll O B D', 'ncoll A B C', 'sameside A O C B O D'), conclusions_txt=('para A B C D',), allow_point_repetition=False), Rule(id='r28', description='Overlapping parallels', premises_txt=('para A B A C',), conclusions_txt=('coll A B C',), allow_point_repetition=False), Rule(id='r29', description='Midpoint is an eqratio', premises_txt=('midp M A B', 'midp N C D'), conclusions_txt=('eqratio M A A B N C C D',), allow_point_repetition=False), Rule(id='r30', description='Right triangles common angle II', premises_txt=('eqangle A B P Q C D U V', 'perp P Q U V'), conclusions_txt=('perp A B C D',), allow_point_repetition=False), Rule(id='r31', description='Denominator cancelling', premises_txt=('eqratio A B P Q C D U V', 'cong P Q U V'), conclusions_txt=('cong A B C D',), allow_point_repetition=False), Rule(id='r34', description='AA Similarity of triangles (Direct)', premises_txt=('eqangle B A B C Q P Q R', 'eqangle C A C B R P R Q', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtri A B C P Q R',), allow_point_repetition=True), Rule(id='r35', description='AA Similarity of triangles (Reverse)', premises_txt=('eqangle B A B C Q R Q P', 'eqangle C A C B R Q R P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtrir A B C P Q R',), allow_point_repetition=True), Rule(id='r36', description='ASA Congruence of triangles (Direct)', premises_txt=('eqangle B A B C Q P Q R', 'eqangle C A C B R P R Q', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r37', description='ASA Congruence of triangles (Reverse)', premises_txt=('eqangle B A B C Q R Q P', 'eqangle C A C B R Q R P', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r41', description='Thales theorem III', premises_txt=('para A B C D', 'coll M A D', 'coll N B C', 'eqratio M A M D N B N C', 'sameside M A D N B C'), conclusions_txt=('para M N A B',), allow_point_repetition=False), Rule(id='r42', description='Thales theorem IV', premises_txt=('para A B C D', 'coll M A D', 'coll N B C', 'para M N A B', 'ncoll A B C'), conclusions_txt=('eqratio M A M D N B N C',), allow_point_repetition=False), Rule(id='r43', description='Orthocenter theorem', premises_txt=('perp A B C D', 'perp A C B D', 'ncoll A B C'), conclusions_txt=('perp A D B C',), allow_point_repetition=False), Rule(id='r44', description="Pappus's theorem", premises_txt=('coll A B C', 'coll P Q R', 'coll X A Q', 'coll X P B', 'coll Y A R', 'coll Y P C', 'coll Z B R', 'coll Z C Q'), conclusions_txt=('coll X Y Z',), allow_point_repetition=False), Rule(id='r45', description="Simson's line theorem", premises_txt=('cyclic A B C P', 'coll A L C', 'perp P L A C', 'coll M B C', 'perp P M B C', 'coll N A B', 'perp P N A B'), conclusions_txt=('coll L M N',), allow_point_repetition=False), Rule(id='r46', description='Incenter theorem', premises_txt=('eqangle A B A X A X A C', 'eqangle B A B X B X B C', 'ncoll A B C'), conclusions_txt=('eqangle C B C X C X C A',), allow_point_repetition=False), Rule(id='r47', description='Circumcenter theorem', premises_txt=('midp M A B', 'perp X M A B', 'midp N B C', 'perp X N B C', 'midp P C A'), conclusions_txt=('perp X P C A',), allow_point_repetition=False), Rule(id='r48', description='Centroid theorem', premises_txt=('midp M A B', 'coll M X C', 'midp N B C', 'coll N X A', 'midp P C A'), conclusions_txt=('coll X P B',), allow_point_repetition=False), Rule(id='r49', description='Recognize center of circle (cyclic)', premises_txt=('circle O A B C', 'cyclic A B C D'), conclusions_txt=('cong O A O D',), allow_point_repetition=False), Rule(id='r50', description='Recognize center of cyclic (cong)', premises_txt=('cyclic A B C D', 'cong O A O B', 'cong O C O D', 'npara A B C D'), conclusions_txt=('cong O A O C',), allow_point_repetition=False), Rule(id='r51', description='Midpoint splits in two', premises_txt=('midp M A B',), conclusions_txt=('rconst M A A B 1/2',), allow_point_repetition=False), Rule(id='r52', description='Properties of similar triangles (Direct)', premises_txt=('simtri A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('eqangle B A B C Q P Q R', 'eqangle A B A C P Q P R', 'eqangle A C B C P R Q R', 'eqratio B A B C Q P Q R', 'eqratio B C A C Q R P R'), allow_point_repetition=True), Rule(id='r53', description='Properties of similar triangles (Reverse)', premises_txt=('simtrir A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('eqangle B A B C Q R Q P', 'eqangle A B A C P R P Q', 'eqangle A C B C Q R P R', 'eqratio B A B C Q P Q R', 'eqratio B C A C Q R P R'), allow_point_repetition=True), Rule(id='r54', description='Definition of midpoint', premises_txt=('cong M A M B', 'coll M A B'), conclusions_txt=('midp M A B',), allow_point_repetition=False), Rule(id='r55', description='Properties of midpoint (cong)', premises_txt=('midp M A B',), conclusions_txt=('cong M A M B',), allow_point_repetition=False), Rule(id='r56', description='Properties of midpoint (coll)', premises_txt=('midp M A B',), conclusions_txt=('coll M A B',), allow_point_repetition=False), Rule(id='r57', description='Pythagoras theorem', premises_txt=('PythagoreanPremises A B C',), conclusions_txt=('PythagoreanConclusions A B C',), allow_point_repetition=False), Rule(id='r58', description='Same chord same arc I', premises_txt=('cyclic A B C P Q R', 'cong A B P Q', 'nperp A C B C', 'sameclock C A B R P Q', 'sameside C A B R P Q'), conclusions_txt=('eqangle C A C B R P R Q',), allow_point_repetition=False), Rule(id='r59', description='Same chord same arc II', premises_txt=('cyclic A B C P Q R', 'cong A B P Q', 'nperp A C B C', 'sameclock C B A R P Q', 'nsameside C B A R P Q'), conclusions_txt=('eqangle C A C B R P R Q',), allow_point_repetition=False), Rule(id='r60', description='SSS Similarity of triangles (Direct)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtri A B C P Q R',), allow_point_repetition=True), Rule(id='r61', description='SSS Similarity of triangles (Reverse)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtrir A B C P Q R',), allow_point_repetition=True), Rule(id='r62', description='SAS Similarity of triangles (Direct)', premises_txt=('eqratio B A B C Q P Q R', 'eqangle B A B C Q P Q R', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtri A B C P Q R',), allow_point_repetition=True), Rule(id='r63', description='SAS Similarity of triangles (Reverse)', premises_txt=('eqratio B A B C Q P Q R', 'eqangle B A B C Q R Q P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('simtrir A B C P Q R',), allow_point_repetition=True), Rule(id='r64', description='SSS Congruence of triangles (Direct)', premises_txt=('cong A B P Q', 'cong B C Q R', 'cong C A R P', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r65', description='SSS Congruence of triangles (Reverse)', premises_txt=('cong A B P Q', 'cong B C Q R', 'cong C A R P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r66', description='SAS Congruence of triangles (Direct)', premises_txt=('cong A B P Q', 'cong B C Q R', 'eqangle B A B C Q P Q R', 'ncoll A B C', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r67', description='SAS Congruence of triangles (Reverse)', premises_txt=('cong A B P Q', 'cong B C Q R', 'eqangle B A B C Q R Q P', 'ncoll A B C', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r68', description='Similarity without scaling (Direct)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P Q R', 'diff A B C', 'diff P Q R'), conclusions_txt=('contri A B C P Q R',), allow_point_repetition=True), Rule(id='r69', description='Similarity without scaling (Reverse)', premises_txt=('eqratio B A B C Q P Q R', 'eqratio C A C B R P R Q', 'ncoll A B C', 'cong A B P Q', 'sameclock A B C P R Q', 'diff A B C', 'diff P Q R'), conclusions_txt=('contrir A B C P Q R',), allow_point_repetition=True), Rule(id='r70', description='Projective harmonic conjugate', premises_txt=('coll A L M', 'coll A K N', 'coll B K M', 'coll B L N', 'coll C M N', 'coll D K L', 'coll A B C D'), conclusions_txt=('eqratio A C A D B C B D',), allow_point_repetition=False), Rule(id='r71', description='Resolution of ratios', premises_txt=('eqratio A B A C D E D F', 'coll A B C', 'coll D E F', 'sameside A B C D E F'), conclusions_txt=('eqratio A B B C D E E F',), allow_point_repetition=False), Rule(id='r72', description='Disassembling a circle', premises_txt=('circle O A B C',), conclusions_txt=('cong O A O B', 'cong O B O C'), allow_point_repetition=False), Rule(id='r73', description='Definition of circle', premises_txt=('cong O A O B', 'cong O B O C'), conclusions_txt=('circle O A B C',), allow_point_repetition=False), Rule(id='r74', description='Intersection of angle bisector and perpendicular bisector', premises_txt=('eqangle C A C D C D C B', 'cong D A D B', 'ncoll A B C D', 'nperp A B C D'), conclusions_txt=('cyclic A B C D',), allow_point_repetition=False), Rule(id='r76', description='Locate midpoint of hypotenuse', premises_txt=('cong A M B M', 'coll B M C', 'perp A B A C'), conclusions_txt=('midp M B C',), allow_point_repetition=False), Rule(id='r77', description='Properties of congruent triangles (Direct)', premises_txt=('contri A B C P Q R',), conclusions_txt=('simtri A B C P Q R', 'cong A B P Q'), allow_point_repetition=True), Rule(id='r78', description='Properties of congruent triangles (Reverse)', premises_txt=('contrir A B C P Q R',), conclusions_txt=('simtrir A B C P Q R', 'cong A B P Q'), allow_point_repetition=True), Rule(id='r79', description='Divide congruence equation by segment', premises_txt=('cong A B C D', 'diff X Y', 'diff A B', 'diff C D'), conclusions_txt=('eqratio A B X Y C D X Y',), allow_point_repetition=True), Rule(id='r80', description='Same chord same arc III', premises_txt=('cyclic A B P Q', 'cong A B P Q', 'npara A P B Q'), conclusions_txt=('eqangle P A P B P B Q B',), allow_point_repetition=False), Rule(id='r81', description='Same chord same arc IV', premises_txt=('cyclic A B P Q', 'cong A B P Q', 'sameclock A P B A P Q'), conclusions_txt=('eqangle P A P B Q B P B',), allow_point_repetition=False), Rule(id='r82', description='Parallel from collinear', premises_txt=('coll A B C',), conclusions_txt=('para A B B C', 'para A B A C'), allow_point_repetition=False), Rule(id='r83', description='Betweeness condition I', premises_txt=('coll A B C', 'obtuse_angle A B C'), conclusions_txt=('lequation 1/1 A B 1/1 B C -1/1 A C 0',), allow_point_repetition=False), Rule(id='r84', description='Betweeness condition II', premises_txt=('lequation 1/1 A B 1/1 B C -1/1 A C 0',), conclusions_txt=('coll A B C',), allow_point_repetition=False), Rule(id='r85', description='Generalized Pythagorean theorem I', premises_txt=('perp A B C D',), conclusions_txt=('lequation 1/1 A C * A C 1/1 B D * B D -1/1 A D * A D -1/1 B C * B C 0',), allow_point_repetition=False), Rule(id='r86', description='Generalized Pythagorean theorem II', premises_txt=('lequation 1/1 A C * A C 1/1 B D * B D -1/1 A D * A D -1/1 B C * B C 0', 'ncoll A B C'), conclusions_txt=('perp A B C D',), allow_point_repetition=False), Rule(id='r87', description='Characterization of circumcenter I', premises_txt=('cong O A O C', 'aequation 1/1 A B B C 1/1 C A A O 90o'), conclusions_txt=('circle O A B C',), allow_point_repetition=False), Rule(id='r88', description='Characterization of circumcenter II', premises_txt=('circle O A B C',), conclusions_txt=('aequation 1/1 A B B C 1/1 C A A O 90o',), allow_point_repetition=False), Rule(id='r89', description='Length of a median of a triangle', premises_txt=('midp M A B', 'ncoll A B C'), conclusions_txt=('lequation 2/1 A M * A M -2/1 B C * B C -2/1 A C * A C 1/1 A B * A B 0',), allow_point_repetition=False), Rule(id='r90', description='Parallelogram law', premises_txt=('para A B C D', 'para A D B C', 'ncoll A B C'), conclusions_txt=('lequation 2/1 A B * A B 2/1 B C * B C -1/1 A C * A C -1/1 B D * B D 0',), allow_point_repetition=False), Rule(id='r91', description='Equal angles in an isosceles trapezoid', premises_txt=('cong A B C D', 'para A D B C', 'npara A B C D'), conclusions_txt=('eqangle C A C B B C B D',), allow_point_repetition=False), Rule(id='r92', description='Any diameter of a circle crosses the center', premises_txt=('midp O A B', 'circle O A B C', 'cyclic A B C D', 'cong A B C D'), conclusions_txt=('coll O C D',), allow_point_repetition=False)]

List of all rules that existed at some point in the history of Newclid

DEACTIVATED_RULES: set[Rule] = {Rule(id='r57', description='Pythagoras theorem', premises_txt=('PythagoreanPremises A B C',), conclusions_txt=('PythagoreanConclusions A B C',), allow_point_repetition=False)}

Rules deactivated because they were problematic for current use cases.

TRIAGE_NO_RULE_NEEDED: set[Rule] = {Rule(id='r00', description='Perpendiculars give parallel', premises_txt=('perp A B C D', 'perp C D E F', 'ncoll A B E'), conclusions_txt=('para A B E F',), allow_point_repetition=False), Rule(id='r02', description='Parallel from inclination', premises_txt=('eqangle A B P Q C D P Q',), conclusions_txt=('para A B C D',), allow_point_repetition=False), Rule(id='r08', description='Right triangles common angle I', premises_txt=('perp A B C D', 'perp E F G H', 'npara A B E F'), conclusions_txt=('eqangle A B E F C D G H',), allow_point_repetition=False), Rule(id='r09', description='Sum of angles of a triangle', premises_txt=('eqangle A B C D M N P Q', 'eqangle C D E F P Q R U', 'npara A B E F'), conclusions_txt=('eqangle A B E F M N R U',), allow_point_repetition=False), Rule(id='r10', description='Ratio cancellation', premises_txt=('eqratio A B C D M N P Q', 'eqratio C D E F P Q R U'), conclusions_txt=('eqratio A B E F M N R U',), allow_point_repetition=False), Rule(id='r30', description='Right triangles common angle II', premises_txt=('eqangle A B P Q C D U V', 'perp P Q U V'), conclusions_txt=('perp A B C D',), allow_point_repetition=False), Rule(id='r31', description='Denominator cancelling', premises_txt=('eqratio A B P Q C D U V', 'cong P Q U V'), conclusions_txt=('cong A B C D',), allow_point_repetition=False), Rule(id='r72', description='Disassembling a circle', premises_txt=('circle O A B C',), conclusions_txt=('cong O A O B', 'cong O B O C'), allow_point_repetition=False), Rule(id='r73', description='Definition of circle', premises_txt=('cong O A O B', 'cong O B O C'), conclusions_txt=('circle O A B C',), allow_point_repetition=False)}

Rules that can be proven by the functioning of the engine and AR (no rule needed).

TRIAGE_LEAVE_RULE_OUT: set[Rule] = {Rule(id='r00', description='Perpendiculars give parallel', premises_txt=('perp A B C D', 'perp C D E F', 'ncoll A B E'), conclusions_txt=('para A B E F',), allow_point_repetition=False), Rule(id='r01', description='Definition of cyclic', premises_txt=('cong O A O B', 'cong O B O C', 'cong O C O D'), conclusions_txt=('cyclic A B C D',), allow_point_repetition=False), Rule(id='r02', description='Parallel from inclination', premises_txt=('eqangle A B P Q C D P Q',), conclusions_txt=('para A B C D',), allow_point_repetition=False), Rule(id='r05', description='Same arc same chord', premises_txt=('cyclic A B C P Q R', 'eqangle C A C B R P R Q'), conclusions_txt=('cong A B P Q',), allow_point_repetition=False), Rule(id='r06', description='Base of half triangle', premises_txt=('midp E A B', 'midp F A C'), conclusions_txt=('para E F B C',), allow_point_repetition=False), Rule(id='r08', description='Right triangles common angle I', premises_txt=('perp A B C D', 'perp E F G H', 'npara A B E F'), conclusions_txt=('eqangle A B E F C D G H',), allow_point_repetition=False), Rule(id='r09', description='Sum of angles of a triangle', premises_txt=('eqangle A B C D M N P Q', 'eqangle C D E F P Q R U', 'npara A B E F'), conclusions_txt=('eqangle A B E F M N R U',), allow_point_repetition=False), Rule(id='r10', description='Ratio cancellation', premises_txt=('eqratio A B C D M N P Q', 'eqratio C D E F P Q R U'), conclusions_txt=('eqratio A B E F M N R U',), allow_point_repetition=False), Rule(id='r13', description='Isosceles triangle equal angles', premises_txt=('cong O A O B', 'ncoll O A B'), conclusions_txt=('eqangle O A A B A B O B',), allow_point_repetition=False), Rule(id='r14', description='Equal base angles imply isosceles', premises_txt=('eqangle A O A B B A B O', 'ncoll O A B'), conclusions_txt=('cong O A O B',), allow_point_repetition=False), Rule(id='r15', description='Arc determines inscribed angles (tangent)', premises_txt=('circle O A B C', 'perp O A A X'), conclusions_txt=('eqangle A X A B C A C B',), allow_point_repetition=False), Rule(id='r16', description='Same arc giving tangent', premises_txt=('circle O A B C', 'eqangle A X A B C A C B'), conclusions_txt=('perp O A A X',), allow_point_repetition=False), Rule(id='r17', description='Central angle vs inscribed angle I', premises_txt=('circle O A B C', 'midp M B C'), conclusions_txt=('eqangle A B A C O B O M',), allow_point_repetition=False), Rule(id='r18', description='Central angle vs inscribed angle II', premises_txt=('circle O A B C', 'coll M B C', 'eqangle A B A C O B O M'), conclusions_txt=('midp M B C',), allow_point_repetition=False), Rule(id='r21', description='Cyclic trapezoid', premises_txt=('cyclic A B C D', 'para A B C D'), conclusions_txt=('eqangle A D C D C D C B',), allow_point_repetition=False), Rule(id='r22', description='Bisector construction', premises_txt=('midp M A B', 'perp O M A B'), conclusions_txt=('cong O A O B',), allow_point_repetition=False), Rule(id='r23', description='Bisector is perpendicular', premises_txt=('cong A P B P', 'cong A Q B Q'), conclusions_txt=('perp A B P Q',), allow_point_repetition=False), Rule(id='r24', description='Cyclic kite', premises_txt=('cong A P B P', 'cong A Q B Q', 'cyclic A B P Q'), conclusions_txt=('perp P A A Q',), allow_point_repetition=False), Rule(id='r29', description='Midpoint is an eqratio', premises_txt=('midp M A B', 'midp N C D'), conclusions_txt=('eqratio M A A B N C C D',), allow_point_repetition=False), Rule(id='r30', description='Right triangles common angle II', premises_txt=('eqangle A B P Q C D U V', 'perp P Q U V'), conclusions_txt=('perp A B C D',), allow_point_repetition=False), Rule(id='r31', description='Denominator cancelling', premises_txt=('eqratio A B P Q C D U V', 'cong P Q U V'), conclusions_txt=('cong A B C D',), allow_point_repetition=False), Rule(id='r45', description="Simson's line theorem", premises_txt=('cyclic A B C P', 'coll A L C', 'perp P L A C', 'coll M B C', 'perp P M B C', 'coll N A B', 'perp P N A B'), conclusions_txt=('coll L M N',), allow_point_repetition=False), Rule(id='r47', description='Circumcenter theorem', premises_txt=('midp M A B', 'perp X M A B', 'midp N B C', 'perp X N B C', 'midp P C A'), conclusions_txt=('perp X P C A',), allow_point_repetition=False), Rule(id='r48', description='Centroid theorem', premises_txt=('midp M A B', 'coll M X C', 'midp N B C', 'coll N X A', 'midp P C A'), conclusions_txt=('coll X P B',), allow_point_repetition=False), Rule(id='r55', description='Properties of midpoint (cong)', premises_txt=('midp M A B',), conclusions_txt=('cong M A M B',), allow_point_repetition=False), Rule(id='r72', description='Disassembling a circle', premises_txt=('circle O A B C',), conclusions_txt=('cong O A O B', 'cong O B O C'), allow_point_repetition=False), Rule(id='r73', description='Definition of circle', premises_txt=('cong O A O B', 'cong O B O C'), conclusions_txt=('circle O A B C',), allow_point_repetition=False), Rule(id='r76', description='Locate midpoint of hypotenuse', premises_txt=('cong A M B M', 'coll B M C', 'perp A B A C'), conclusions_txt=('midp M B C',), allow_point_repetition=False)}

Rules that can be proven by other rules, so are redundant.