통합 해제(컴퓨터 과학)

컴퓨터 과학과 논리학에서, 불통일은 상징적 표현들 사이의 불평등을 해결하는 알고리즘 과정이다.

통일 해제에 관한 출판물

• Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). Proc. Int. Conf. on Fifth Generation Computer Systems. pp. 85–99.
• Hubert Comon (1986). "Sufficient Completeness, Term Rewriting Systems and 'Anti-Unification'". Proc. 8th International Conference on Automated Deduction. LNCS. Vol. 230. Springer. pp. 128–140.
  여기서 "반통일"은 불평등 해소를 의미하는데, 이것은 요즘 매우 이례적인 명칭이다.반통일(컴퓨터 과학).
• Claude Kirchner; Pierre Lescanne (1987). "Solving Disequations". Proc. LICS. pp. 347–352.
• Claude Kirchner and Pierre Lescanne (1987). Solving disequations (Research Report). INRIA.
• Hubert Comon (1988). Unification et disunification: Théorie et applications (PDF) (Ph.D.). I.N.P. de Grenoble.
• Hubert Comon; Pierre Lescanne (Mar–Apr 1989). "Equational Problems and Disunification". J. Symb. Comput. 7 (3–4): 371–425.
• Comon, Hubert (1990). "Equational Formulas in Order-Sorted Algebras". Proc. ICALP.
  Comon은 평등과 소트 멤버쉽의 1차 논리이론이 결정가능하다는 것을 보여준다. 즉, 임의의 함수 기호인 "="와 "delect"로 만들어진 각 1차 논리식은 다른 어떤 술어도 효과적으로 증명되거나 반증될 수 없다.논리 부정(),)을 사용하면 비등식())을 공식으로 표현할 수 있지만 순서 관계(<)는 표현할 수 없다.응용 프로그램으로서 용어 개서 시스템의 충분한 완성도를 증명한다.
• Hubert Comon (1991). "Disunification: A Survey". In Jean-Louis Lassez; Gordon Plotkin (eds.). Computational Logic — Essays in Honor of Alan Robinson. MIT Press. pp. 322–359.
• Hubert Comon (1993). "Complete Axiomatizations of some Quotient Term Algebras" (PDF). Proc. 18th Int. Coll. on Automata, Languages, and Programming. LNCS. Vol. 510. Springer. pp. 148–164. Retrieved 29 June 2013.

「 」를 참조해 주세요.

• 통일(컴퓨터 사이언스): 기호 표현 사이의 방정식을 푼다.
• 제약 로직 프로그래밍: 특정 부등식 클래스(및 기타 관계)에 대한 해결 알고리즘을 프롤로그에 통합
• 제약 프로그래밍: 부등식의 특정 클래스에 대한 알고리즘 해결
• 심플렉스 알고리즘: 선형 부등식에 대한 해결 알고리즘
• 부등식: 수학의 일반적인 부등식의 종류로, 풀이에 관한 간단한 섹션을 포함한다.
• 방정식 풀기: 수학에서 방정식을 푸는 방법