Разъединение

Дезунификация в информатике и логике — это алгоритмический процесс решения неравенств между символическими выражениями .

• Ален Колмерауэр (1984). «Уравнения и неравенства на конечных и бесконечных деревьях». В ICOT (ред.). Труды Междунар. конференции по компьютерным системам пятого поколения . стр. 85–99.
• Хьюберт Комон (1986). «Достаточная полнота, системы переписывания терминов и «антиунификация»". Труды 8-й Международной конференции по автоматизированной дедукции . LNCS . Том 230. Springer. С. 128–140.
  «Антиунификация» здесь относится к решению неравенств, название, которое в настоящее время стало довольно необычным, ср. Антиунификация (компьютерная наука) .
• Клод Киршнер; Пьер Лескан (1987). «Решение дизэкваций». Учеб. ЛИКС . стр. 347–352.
• Клод Киршнер и Пьер Лескан (1987). Решение проблем (Отчет об исследовании). ИНРИА.
• Хьюберт Комон (1988). Унификация и разъединение: Теория и приложения (PDF) (доктор философии). ИЯФ Гренобля.
• Hubert Comon; Pierre Lescanne (март–апрель 1989 г.). «Equational Problems and Disunification» (Проблемы уравнения и разъединение). J. Symb. Comput. 7 (3–4): 371–425. CiteSeerX  10.1.1.139.4769 . doi : 10.1016/S0747-7171(89)80017-3 .
• Комон, Хьюберт (1990). «Формулы уравнений в упорядоченно-отсортированных алгебрах». Труды ICALP .
  Комон показывает, что теория равенства и принадлежности к сорту в логике первого порядка разрешима, то есть каждая формула логики первого порядка, построенная из произвольных символов функций, "=" и "∈", но не из других предикатов, может быть эффективно доказана или опровергнута. Используя логическое отрицание (¬), неравенство (≠) можно выразить в формулах, но отношения порядка (<) — нет. В качестве приложения он доказывает достаточную полноту систем переписывания терминов .
• Хьюберт Комон (1991). «Разъединение: обзор». В Жан-Луи Лассе; Гордон Плоткин (ред.). Вычислительная логика — Эссе в честь Алана Робинсона . MIT Press. стр. 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 . Получено 29 июня 2013 г. .

• Унификация (информатика) : решение уравнений между символическими выражениями
• Программирование логики ограничений : включение алгоритмов решения для определенных классов неравенств (и других отношений) в Пролог
• Программирование в ограничениях : алгоритмы решения для определенных классов неравенств
• Симплексный алгоритм : алгоритм решения линейных неравенств
• Неравенство : виды неравенств в математике в целом, включая краткий раздел по решению
• Решение уравнений : как решать уравнения в математике