alpha-geometry

Example Deduction Engine⚑

• http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf

• predicates 로 다음과 같은 것들이 소개된다

  • points (A, B, C) - 세 점 A, B, C 가 존재한다.
  • coll (E, A, C) - 점 E, A, C 가 같은 선상에 존재한다.
  • para (A, B, C, D) - AB 와 CD 가 평행하다.
  • perp (A, B, C, D) - AB 와 CD 가 수직이다.
  • midp (M, A, B) - M 은 A와 B의 중점이다.

• premise 는 전제를 의미한다. 문제에서 주어진 조건들을 형식적으로 변환한 것을 의미한다.

  • 다음과 같은 예시를 생각해볼 수 있다.

  premises = [
      ("triangle", "A", "B", "C"),
      ("interior_angle", "angle_ABC", "C")
  ]
  

  • triangle 은 세 점이 삼각형을 이룬다는 것을 의미한다.
  • interior_angle 은 내각을 의미한다. ABC 의 내각이 C 라는 것을 의미한다.

• conclusion 은 결론을 의미한다. 문제에서 구해야 하는 것을 형식적으로 표현한 것을 의미한다.

  • 다음과 같은 예시를 생각해볼 수 있다.

  goal = ("exterior_angle", "angle_ABC", "angle_BCA", "angle_CAB")
  

  • exterior_angle 은 외각을 의미한다. ABC 의 외각이 BCA 와 CAB 의 합이라는 것을 의미한다.

• deduction rule 은 추론 규칙을 의미한다.

  • 전제로부터 결론을 도출하는 방법을 의미한다.
  • 아래와 같이, 어떤 전제가 주어질 때 도출할 수 있는 연역적 규칙들을 의미한다.
  • Modus_ponens 와 같은 추론 규칙을 생각해볼 수 있다.

  def exterior_angle_of_triangle(premises):
  new_conclusions = []
  for premise1 in premises:
      if premise1[0] == "triangle":
          A, B, C = premise1[1], premise1[2], premise1[3]
          # 추가적인 전제를 검사합니다.
          for premise2 in premises:
              if premise2[0] == "interior_angle":
                  interior_angle, vertex = premise2[1], premise2[2]
                  if vertex == C and interior_angle == f"angle_{A}{B}{C}":
                      new_conclusions.append(
                          (
                              "exterior_angle",
                              f"angle_{B}{A}{C}",
                              f"angle_{A}{B}{C}",
                              f"angle_{B}{C}{A}",
                          )
                      )
  return new_conclusions
  

• solver 는 주어진 premises 와 deduction rule 을 반복적으로 적용하여 goal 을 도출하는 과정을 의미

  # Solver
  def apply_deduction_rules(premises, goal=None, max_iterations=10000):
      conclusions = []
      seen_premises = set(premises)
      iterations = 0
  
      while True:
          new_conclusions = []
          iterations += 1
  
          # Apply each deduction strategy
          for strategy in [
              sum_of_angles_in_triangle,
              exterior_angle_of_triangle,
          ]:
              strategy_conclusions = strategy(premises)
              for conclusion in strategy_conclusions:
                  if conclusion not in seen_premises:
                      new_conclusions.append(conclusion)
                      seen_premises.add(conclusion)
                      # Check if the goal has been achieved
                      if goal and conclusion == goal:
                          conclusions.append(conclusion)
                          return conclusions
  
          # If no new conclusions, break the loop
          if not new_conclusions:
              break
  
          # If maximum iterations reached, break the loop
          if iterations >= max_iterations:
              print("Max iterations reached, stopping deduction")
              break
  
          conclusions.extend(new_conclusions)
          premises.extend(new_conclusions)  # Update premises with new conclusions
  
      return conclusions
  
  def traceback(conclusions, premises):
      proof = premises.copy()
      for conclusion in conclusions:
          if conclusion not in proof:
              proof.append(conclusion)
      return proof
  

• 종합적으로 Deduction Engine 을 이용해 문제를 푸는 과정은 다음과 같이 생각해볼 수 있다.

  # 예시: 다양한 전제와 추론 규칙 적용
  premises = [
      ("triangle", "A", "B", "C"),
      ("interior_angle", "angle_ABC", "C")  # 내각의 전제를 추가합니다.
  ]
  goal = ("exterior_angle", "angle_ABC", "angle_BCA", "angle_CAB")
  conclusions = apply_deduction_rules(premises, goal)
  proof = traceback(conclusions, premises)
  
  print(f"Proof:")
  for step in proof:
      print(step)
  

• M 이 AB 의 중점이고, O 가 AB 에 수직이라면, OA 와 OB 는 같다는 것을 도출하는 deduction rule 을 도출하는 코드이다.
• 해당 코드는 여기 에서 확인할 수 있다.

def match_midp_perp_cong(
    g: gh.Graph,
    g_matcher: Callable[str, list[tuple[gm.Point, ...]]],
    theorem: pr.Theorem,
) -> Generator[dict[str, gm.Point], None, None]:
  """Match midp M A B, perp O M A B => cong O A O B."""
  for m, a, b in g.all_midps():
    ab = g._get_line(a, b)
    for l in m.neighbors(gm.Line):
      if g.check_perpl(l, ab):
        for o in l.neighbors(gm.Point):
          if o != m:
            yield dict(zip('ABMO', [a, b, m, o]))

class GeometricTable(Table):
  """Abstract class representing the coefficient matrix (table) A."""
  # ... 생략
  def get_all_eqs_and_why(
      self, return_quads: bool
  ) -> Generator[Any, None, None]:
    for out in super().get_all_eqs_and_why(return_quads):
      if len(out) == 3:
        x, y, why = out
        x, y = self.map2obj([x, y])
        yield x, y, why
      if len(out) == 4:
        x, y, f, why = out
        x, y = self.map2obj([x, y])
        yield x, y, f, why
      if len(out) == 5:
        a, b, x, y, why = out
        a, b, x, y = self.map2obj([a, b, x, y])
        yield a, b, x, y, why

• 아래 예시를 보면 add_eq, add_const_ratio, add_eqratio 를 통해서 전제를 추가하고, get_all_eqs_and_why 를 통해 새롭게 결론을 도출하는 AR 과정을 확인할 수 있다.
• 실제 코드 예시는 여기 있다.

class RatioTable(GeometricTable):
  """Coefficient matrix A for log(distance)."""

  def __init__(self, name: str = ''):
    name = name or '1'
    super().__init__(name)
    self.one = self.const

  def add_eq(self, l1: gm.Length, l2: gm.Length, dep: pr.Dependency) -> None:
    l1, l2 = self.get_name([l1, l2])
    return super().add_eq3(l1, l2, 0.0, dep)

  def add_const_ratio(
      self, l1: gm.Length, l2: gm.Length, m: float, n: float, dep: pr.Dependency
  ) -> None:
    l1, l2 = self.get_name([l1, l2])
    return super().add_eq2(l1, l2, m, n, dep)

  def add_eqratio(
      self,
      l1: gm.Length,
      l2: gm.Length,
      l3: gm.Length,
      l4: gm.Length,
      dep: pr.Dependency,
  ) -> None:
    l1, l2, l3, l4 = self.get_name([l1, l2, l3, l4])
    return self.add_eq4(l1, l2, l3, l4, dep)

  def get_all_eqs_and_why(self) -> Generator[Any, None, None]:
    return super().get_all_eqs_and_why(True)

• 실제로 AR 이 적용되는 코드는 여기 에서 확인할 수 있다.