스택큐힙리스트

나는 고차원 정리 증명기를 개발 중이며, 그 중에서 통일은 가장 어려운 하위 문제로 보입니다. 휘에의 알고리즘이 여전히 최첨단 기술로 간주된다면, 프로그래머가 이해하기 쉽도록 작성된 해당 알고리즘에 대한 설명 링크가 있는 사람은 있을까요? 또는 첫 번째 주문 알고리즘이 작동하지 않는 경우의 예제도 있을까요?답변 1최첨단 - 네, 내가 알기로는 모든 알고리즘은 거의 Huet의 것과 동일한 형태를 가지고 있다. (나는 논리 프로그래밍 이론을 따르지만, 나의 전문분야는 겸하고 있다) 만약 완전한 고차원 매칭이 필요하다면, 고차원 매칭과 같은 하위 문제들 (닫힌 한 가지 항을 가지는 단위화), Dale Miller의 패턴 미적분은 결정 가능하다. Huet의 알고리즘은 다음과 같은 의미에서 최고의 것이다 - 만약..