Problem Solving Examples

Click on the buttons below to switch between different problems and views.

#### Problem Description

Find the measure of ∠CFD on ⊙F with diameter AC.

    PointLiesOnCircle(D, Circle(F, radius_0_0))
    PointLiesOnCircle(A, Circle(F, radius_0_0))
    PointLiesOnCircle(C, Circle(F, radius_0_0))
    PointLiesOnCircle(B, Circle(F, radius_0_0))
    Equals(MeasureOf(Angle(D, F, C)), 4a-1)
    Equals(MeasureOf(Arc(A, D)), 2a-5)
    Equals(MeasureOf(Angle(C, F, B)), 72)
    Circle(F)
    IsDiameterOf(Line(A,C),Circle(F))
    Find(MeasureOf(Angle(C,F,D)))

    1: Known facts: start ⇒ ∠DFC, pi * ((4 * a - 1) / 180) = ∠DFC, 3.14 = pi, pi * ((2 * a - 5) / 180) = ∠AFD, ∠AFD
    2: Substitution: pi * ((4 * a - 1) / 180) = ∠DFC, 3.14 = pi ⇒ 3.14 * ((4 * a - 1) / 180) = ∠DFC
    3: Substitution: 3.14 = pi, pi * ((2 * a - 5) / 180) = ∠AFD ⇒ 3.14 * ((2 * a - 5) / 180) = ∠AFD
    4: Straight Angle: ∠DFC, ∠AFD ⇒ pi = ∠AFD + ∠DFC
    5: Transtivity of Equivalence: 3.14 = pi, pi = ∠AFD + ∠DFC ⇒ 3.14 = ∠AFD + ∠DFC
    6: Solve Linear Equation System: 3.14 = ∠AFD + ∠DFC, 3.14 * ((4 * a - 1) / 180) = ∠DFC, 3.14 * ((2 * a - 5) / 180) = ∠AFD ⇒ 2.15 = ∠DFC
    Final answer: 2.15

#### Problem Description

Circle O has a radius of 13 inches. Radius O B is perpendicular to chord C D which is 24 inches long. Find O X.

    Equals(LengthOf(Line(C, D)), 24)
    Equals(LengthOf(Line(O, B)), 13)
    Equals(RadiusOf(Circle(O)), 13)
    IsChordOf(Line(C, D), Circle(O))
    Perpendicular(Line(B, X), Line(D, X))
    Perpendicular(Line(O, B), Line(C, D))
    PointLiesOnCircle(B, Circle(O, radius_0_0))
    PointLiesOnCircle(C, Circle(O, radius_0_0))
    PointLiesOnCircle(D, Circle(O, radius_0_0))
    PointLiesOnLine(X, Line(B, O))
    PointLiesOnLine(X, Line(C, D))
    Find(LengthOf(Line(O, X)))

    1: Known facts: start ⇒ 13 = radius_0_0, CD, DO, D on ⊙(O, radius_0_0), CX ⊥ OX, CO, OX, ∠OCX, C on ⊙(O, radius_0_0), ∠OCD, 24 = CD, CX, X on CD
    2: Point On Circle Def: D on ⊙(O, radius_0_0) ⇒ radius_0_0 = DO
    3: Definition of Triangle: DO, CD, CO ⇒ △CDO
    4: Point On Circle Def: C on ⊙(O, radius_0_0) ⇒ radius_0_0 = CO
    5: Definition of Triangle: CO, OX, CX ⇒ △COX
    6: Same Angle: ∠OCD, X on CD ⇒ ∠OCD = ∠OCX
    7: Transtivity of Equivalence: radius_0_0 = DO, 13 = radius_0_0 ⇒ 13 = DO
    8: Law of Cosines: △CDO ⇒ (CD ** 2 + CO ** 2) - DO ** 2 = 2 * CD * CO * cos(∠OCD)
    9: Transtivity of Equivalence: 13 = radius_0_0, radius_0_0 = CO ⇒ 13 = CO
    10: Sin Function Definition: ∠OCX, △COX, CX ⊥ OX ⇒ OX / CO = sin(∠OCX)
    11: Substitution: 13 = CO, ∠OCD = ∠OCX, (CD ** 2 + CO ** 2) - DO ** 2 = 2 * CD * CO * cos(∠OCD), 13 = DO, 24 = CD ⇒ (13 ** 2 + 24 ** 2) - 13 ** 2 = 13 * 2 * 24 * cos(∠OCX)
    12: Solve Univariate Equation: (13 ** 2 + 24 ** 2) - 13 ** 2 = 13 * 2 * 24 * cos(∠OCX) ⇒ 0.39 = ∠OCX
    13: Substitution: 0.39 = ∠OCX, 13 = CO, OX / CO = sin(∠OCX) ⇒ sin(0.39) = OX / 13
    14: Solve Linear Equation System: sin(0.39) = OX / 13 ⇒ 5 = OX
    Final answer: 5

#### Problem Description

Find x. Assume that segments that appear to be tangent are tangent.

    Equals(LengthOf(Line(A, B)), x)
    Equals(LengthOf(Line(A, F)), 8)
    Equals(LengthOf(Line(C, B)), 6)
    Equals(LengthOf(Line(E, F)), 8)
    PointLiesOnCircle(B, Circle(C, radius_0_0))
    PointLiesOnCircle(D, Circle(C, radius_0_0))
    PointLiesOnCircle(F, Circle(C, radius_0_0))
    PointLiesOnLine(B, Line(A, C))
    PointLiesOnLine(D, Line(C, E))
    PointLiesOnLine(F, Line(A, E))
    Tangent(Line(A, B), Circle(C, radius_0_0))
    Tangent(Line(A, F), Circle(C, radius_0_0))
    Tangent(Line(C, E), Circle(C, radius_0_0))
    Find(x)

    1: Known facts: start ⇒ B on ⊙(C, radius_0_0), Tangent(AF, ⊙(C, radius_0_0)), B on AC, AC, AF, 8 = AF, CF, x = AB, 6 = BC, F on ⊙(C, radius_0_0)
    2: Point On Circle Def: B on ⊙(C, radius_0_0) ⇒ radius_0_0 = BC
    3: Line Segment Split: B on AC ⇒ AC = AB + BC
    4: Definition of Triangle: AF, CF, AC ⇒ △ACF
    5: Tangent Definition: Tangent(AF, ⊙(C, radius_0_0)), F on ⊙(C, radius_0_0) ⇒ AF ⊥ CF
    6: Point On Circle Def: F on ⊙(C, radius_0_0) ⇒ radius_0_0 = CF
    7: Transtivity of Equivalence: radius_0_0 = BC, 6 = BC ⇒ 6 = radius_0_0
    8: Substitution: x = AB, AC = AB + BC, 6 = BC ⇒ 6 + x = AC
    9: Pythagorean Theorem: AF ⊥ CF, △ACF ⇒ AC ** 2 = AF ** 2 + CF ** 2
    10: Transtivity of Equivalence: 6 = radius_0_0, radius_0_0 = CF ⇒ 6 = CF
    11: Substitution: 6 + x = AC, 6 = CF, AC ** 2 = AF ** 2 + CF ** 2, 8 = AF ⇒ 6 ** 2 + 8 ** 2 = (6 + x) ** 2
    12: Solve Univariate Equation: 6 ** 2 + 8 ** 2 = (6 + x) ** 2 ⇒ 4 = x
    Final answer: 4

#### Problem Description

Use parallelogram J K L M to find measure of ∠ K J L if J K = 2 b + 3 and J M = 3 a.

    PointLiesOnLine(R, Line(M, K))
    PointLiesOnLine(R, Line(J, L))
    Equals(LengthOf(Line(L, K)), 21)
    Equals(LengthOf(Line(M, J)), 3a)
    Equals(LengthOf(Line(M, L)), 45)
    Equals(LengthOf(Line(J, K)), 2b+3)
    Equals(MeasureOf(Angle(R, L, M)), 30)
    Equals(MeasureOf(Angle(R, L, K)), 70)
    Parallelogram(J,K,L,M)
    Equals(LengthOf(Line(J,K)),2b+3)
    Equals(LengthOf(Line(J,M)),3a)
    Find(MeasureOf(Angle(K,J,L)))

    1: Known facts: start ⇒ Parallelogram(J, K, L, M), ∠JLM, pi * (30 / 180) = ∠RLM, ∠LJK, R on JL
    2: Parallelogram Opposite Lines Parallel: Parallelogram(J, K, L, M) ⇒ JK || ML
    3: Same Angle: R on JL, ∠LJK ⇒ ∠LJK = ∠RJK
    4: Same Angle: ∠JLM, R on JL ⇒ ∠JLM = ∠RLM
    5: Alternate Interior Angle Theorem: JK || ML ⇒ ∠JLM = ∠LJK
    6: Transtivity of Equivalence: ∠LJK = ∠RJK, ∠JLM = ∠LJK ⇒ ∠JLM = ∠RJK
    7: Transtivity of Equivalence: ∠JLM = ∠RLM, pi * (30 / 180) = ∠RLM, ∠JLM = ∠RJK ⇒ pi * (30 / 180) = ∠RJK
    8: Transtivity of Equivalence: pi * (30 / 180) = ∠RJK, ∠LJK = ∠RJK ⇒ pi * (30 / 180) = ∠LJK
    9: Evaluate: pi * (30 / 180) = ∠LJK ⇒ 0.52 = ∠LJK
    Final answer: 0.52

#### Problem Description

Find B D if B F bisects ∠ A B C and A C || E D, B A = 6, B C = 7.5, A C = 9, and D E = 9.

    PointLiesOnLine(C, Line(B, D))
    PointLiesOnLine(F, Line(A, C))
    PointLiesOnLine(F, Line(E, B))
    Parallel(Line(E, D), Line(A, C))
    Equals(MeasureOf(Angle(A, B, F)), MeasureOf(Angle(C, B, F)))
    BisectsAngle(Line(B,F),Angle(A,B,C))
    Parallel(Line(A,C),Line(E,D))
    Equals(LengthOf(Line(B,A)),6)
    Equals(LengthOf(Line(B,C)),7.5)
    Equals(LengthOf(Line(A,C)),9)
    Equals(LengthOf(Line(D,E)),9)
    Find(LengthOf(Line(B,D)))

    1: Known facts: start ⇒ 7.5 = BC, 9 = DE, F on BE, ∠DBF, F on AC, C on BD, ∠BCA, AB, ∠CBF = ∠FBA, AC, BC, ∠DBE, 9 = AC, 6 = AB, AC || ED
    2: Line Segment Split: F on AC ⇒ AC = AF + CF
    3: Same Angle: ∠DBF, C on BD ⇒ ∠CBF = ∠DBF
    4: Same Angle: ∠BCA, F on AC ⇒ ∠BCA = ∠BCF
    5: Definition of Triangle: AB, BC, AC ⇒ △ABC
    6: Same Angle: F on BE, ∠DBE ⇒ ∠DBE = ∠DBF
    7: Corresponding Angle Theorem: AC || ED ⇒ ∠BCA = ∠BDE, ∠BED = ∠BFC
    8: Transtivity of Equivalence: 9 = AC, AC = AF + CF ⇒ 9 = AF + CF
    9: Triangle Angle Bisector Theorem: ∠CBF = ∠FBA, △ABC ⇒ BC / AB = CF / AF
    10: Transtivity of Equivalence: ∠DBE = ∠DBF, ∠CBF = ∠DBF ⇒ ∠CBF = ∠DBE
    11: Transtivity of Equivalence: ∠BCA = ∠BDE, ∠BCA = ∠BCF ⇒ ∠BCF = ∠BDE
    12: Substitution: BC / AB = CF / AF, 6 = AB, 7.5 = BC ⇒ 7.5 / 6 = CF / AF
    13: Angle-Angle Similarity Theorem: ∠CBF = ∠DBE, ∠BCF = ∠BDE, ∠BED = ∠BFC ⇒ △BCF ~ △BDE
    14: Similar Definition: △BCF ~ △BDE ⇒ ∠BED = ∠BFC, ∠CBF = ∠DBE, sim_ratio_triangle_b_c_f_triangle_b_d_e = CF / DE, sim_ratio_triangle_b_c_f_triangle_b_d_e = BC / BD
    15: Substitution: sim_ratio_triangle_b_c_f_triangle_b_d_e = CF / DE, 9 = DE ⇒ sim_ratio_triangle_b_c_f_triangle_b_d_e = CF / 9
    16: Substitution: sim_ratio_triangle_b_c_f_triangle_b_d_e = BC / BD, 7.5 = BC ⇒ sim_ratio_triangle_b_c_f_triangle_b_d_e = 7.5 / BD
    17: Solve Linear Equation System: 7.5 / 6 = CF / AF, sim_ratio_triangle_b_c_f_triangle_b_d_e = CF / 9, 9 = AF + CF ⇒ 0.56 = sim_ratio_triangle_b_c_f_triangle_b_d_e
    18: Transtivity of Equivalence: 0.56 = sim_ratio_triangle_b_c_f_triangle_b_d_e, sim_ratio_triangle_b_c_f_triangle_b_d_e = 7.5 / BD ⇒ 0.56 = 7.5 / BD
    19: Solve Linear Equation System: 0.56 = 7.5 / BD ⇒ 13.5 = BD
    Final answer: 13.5

#### Problem Description

Find Q P.

    PointLiesOnLine(Q, Line(M, P))
    PointLiesOnLine(N, Line(M, O))
    Parallel(Line(Q, N), Line(P, O))
    Equals(LengthOf(Line(M, N)), 6)
    Equals(LengthOf(Line(M, Q)), 5)
    Equals(LengthOf(Line(O, N)), 3+\frac{3}{5})
    Equals(LengthOf(Line(P, Q)), x)
    Find(LengthOf(Line(Q,P)))

    1: Known facts: start ⇒ 3 + 3 / 5 = NO, 5 = MQ, ∠QMO, ∠OPM, 6 = MN, ∠PMO, ∠OPM, NQ || OP, N on MO, ∠NQM, 3.14 = pi, x = PQ, Q on MP
    2: Reverse Angle Definition: ∠OPM ⇒ ∠OPM = 2 * pi - ∠MPO
    3: Corresponding Angle Theorem: NQ || OP ⇒ ∠MNQ = ∠MOP, ∠MPO = ∠MQN
    4: Line Segment Split: N on MO ⇒ MO = MN + NO
    5: Same Angle: N on MO, ∠QMO ⇒ ∠QMN = ∠QMO
    6: Reverse Angle Definition: ∠NQM ⇒ ∠NQM = 2 * pi - ∠MQN
    7: Same Angle: Q on MP, ∠OPM ⇒ ∠OPM = ∠OPQ
    8: Same Angle: Q on MP, ∠PMO ⇒ ∠PMO = ∠QMO
    9: Line Segment Split: Q on MP ⇒ MP = MQ + PQ
    10: Substitution: 3 + 3 / 5 = NO, MO = MN + NO, 6 = MN ⇒ 6 + (3 + 3 / 5) = MO
    11: Substitution: ∠NQM = 2 * pi - ∠MQN, 3.14 = pi ⇒ ∠NQM = 2 * 3.14 - ∠MQN
    12: Substitution: 3.14 = pi, ∠MPO = ∠MQN, ∠OPM = 2 * pi - ∠MPO, ∠OPM = ∠OPQ ⇒ ∠OPQ = 2 * 3.14 - ∠MQN
    13: Transtivity of Equivalence: ∠QMN = ∠QMO, ∠PMO = ∠QMO ⇒ ∠PMO = ∠QMN
    14: Substitution: 5 = MQ, MP = MQ + PQ, x = PQ ⇒ 5 + x = MP
    15: Solve Linear Equation System: 6 + (3 + 3 / 5) = MO ⇒ 9.6 = MO
    16: Transtivity of Equivalence: ∠NQM = 2 * 3.14 - ∠MQN, ∠OPQ = 2 * 3.14 - ∠MQN ⇒ ∠NQM = ∠OPQ
    17: Transtivity of Equivalence: ∠NQM = ∠OPQ, ∠OPM = ∠OPQ ⇒ ∠NQM = ∠OPM
    18: Angle-Angle Similarity Theorem: ∠NQM = ∠OPM, ∠MNQ = ∠MOP, ∠PMO = ∠QMN ⇒ △MNQ ~ △MOP
    19: Similar Definition: △MNQ ~ △MOP ⇒ sim_ratio_triangle_m_n_q_triangle_m_o_p = MQ / MP, ∠PMO = ∠QMN, sim_ratio_triangle_m_n_q_triangle_m_o_p = MN / MO, ∠MNQ = ∠MOP, ∠MPO = ∠MQN
    20: Substitution: sim_ratio_triangle_m_n_q_triangle_m_o_p = MQ / MP, 5 = MQ, 5 + x = MP ⇒ sim_ratio_triangle_m_n_q_triangle_m_o_p = 5 / (5 + x)
    21: Substitution: sim_ratio_triangle_m_n_q_triangle_m_o_p = MN / MO, 9.6 = MO, 6 = MN ⇒ 6 / 9.6 = sim_ratio_triangle_m_n_q_triangle_m_o_p
    22: Transtivity of Equivalence: sim_ratio_triangle_m_n_q_triangle_m_o_p = 5 / (5 + x), 6 / 9.6 = sim_ratio_triangle_m_n_q_triangle_m_o_p ⇒ 6 / 9.6 = 5 / (5 + x)
    23: Solve Linear Equation System: 6 / 9.6 = 5 / (5 + x), x = PQ ⇒ 3 = PQ
    Final answer: 3

Code

The code is available in the Supplementary Material and will be released on GitHub after the review process.

Anonymous Authors