分裂

コンピュータ科学や論理学における非統一化とは、記号表現間の不等式を解くアルゴリズム的プロセスである。

• アラン・コルメラウアー（1984）。「有限木と無限木上の等式と不等式」。ICOT（編）。第5世代コンピュータシステムに関する国際会議議事録。pp . 85–99。 
• ヒューバート・コモン（1986）。「十分完全性、用語書き換えシステム、および「反統一」」「.第 8 回自動推論に関する国際会議議事録. LNCS . Vol.  230. Springer. pp. 128–140 . ここでいう「反統一」とは不等式を解くことを指すが、この名称は今日では非常に珍しいものとなっている（反統一（コンピュータサイエンス）を参照） 。
• クロード・キルヒナー。ピエール・レスカンヌ (1987)。 「不平等の解決」。手順リックス。347～ 352ページ。 
• クロード・キルシュナーとピエール・レスカンヌ (1987)。不平等の解決(研究レポート)。インリア。
• ヒューバート・コモン (1988)。統一と不統一: 理論と応用(PDF) (Ph.D.)。 INP ドゥ グルノーブル。
• Hubert Comon; Pierre Lescanne (1989年3月～4月)。「方程式問題と非統一性」。J . Symb. Comput. 7 ( 3–4 ): 371–425。CiteSeerX 10.1.1.139.4769。doi : 10.1016/S0747-7171( 89 ) 80017-3。 
• Comon, Hubert (1990). 「順序ソート代数における等式」. Proc. ICALP .コモンは、等価性と順序メンバーシップに関する一階述語論理の理論が決定可能であることを示している。すなわち、任意の関数記号「="」と「∈」から構成される一階述語論理式は、他の述語から構成される式とは異なり、効果的に証明または反証することができる。論理否定（¬）を用いることで、非等価性（≠）は論理式で表現できるが、順序関係（<）は表現できない。応用として、彼は項書き換えシステムの十分完全性を証明している。
• Hubert Comon (1991). 「分裂：概観」 . Jean-Louis Lassez、Gordon Plotkin (編)『計算論理学 ―アラン・ロビンソン記念論文集』 . 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 . 2013年6月29日取得. 

• 統一（コンピュータ科学）：記号表現間の方程式を解くこと
• 制約論理プログラミング：特定の種類の不等式（およびその他の関係）の解法アルゴリズムをPrologに組み込む
• 制約プログラミング：特定の種類の不等式を解くアルゴリズム
• シンプレックス法：線形不等式の解法
• 不等式：数学における不等式の種類全般、および不等式の解法に関する簡単なセクションを含む
• 方程式の解き方：数学における方程式の解き方