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

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

Публикации о разъединении

• Ален Кольмерауэр (1984). «Уравнения и неравенства на конечных и бесконечных деревьях». В ICOT (ред.). Учеб. Межд. Конф. о компьютерных системах пятого поколения . стр. 85–99.
• Хьюберт Комон (1986). «Достаточная полнота, системы переписывания терминов и «антиунификация» ». Учеб. 8-я Международная конференция по автоматизированному дедукции . ЛНКС . Том. 230. Спрингер. стр. 128–140.
  «Антиобъединение» здесь относится к решению неравенств, название, которое в наши дни стало весьма необычным, ср. Антиунификация (информатика) .
• Клод Киршнер; Пьер Лескан (1987). «Решение дизэкваций». Учеб. ЛИКС . стр. 347–352.
• Клод Киршнер и Пьер Лескан (1987). Решение проблем (Отчет об исследовании). ИНРИА.
• Хьюберт Комон (1988). Объединение и разъединение: теория и приложения (PDF) (доктор философии). Гренобльский ИЯФ.
• Юбер Комон; Пьер Лесканн (март – апрель 1989 г.). «Эквациональные проблемы и разъединение» . Дж. Симб. Вычислить. 7 (3–4): 371–425. CiteSeerX   10.1.1.139.4769 . дои : 10.1016/S0747-7171(89)80017-3 .
• Комон, Хьюберт (1990). «Уравнения в алгебрах с порядковой сортировкой». Учеб. ИКАЛП .
  Комон показывает, что логическая теория равенства и принадлежности к сортировке первого порядка разрешима, то есть каждая логическая формула первого порядка, построенная из произвольных функциональных символов «=" и «ε», но без других предикатов, может быть эффективно доказана или опровергнуто. С помощью логического отрицания (¬) неравенство (≠) можно выразить в формулах, а отношения порядка (<) — нет. В качестве приложения он доказывает достаточную полноту терминов систем переписывания .
• Хьюберт Комон (1991). «Разъединение: обзор» . В Жан-Луи Лассе; Гордон Плоткин (ред.). Вычислительная логика — Очерки в честь Алана Робинсона . МТИ Пресс. стр. 322–359.
• Хьюберт Комон (1993). «Полная аксиоматизация некоторых алгебр с факторными членами» (PDF) . Учеб. 18-й Международный. Колл. по автоматам, языкам и программированию . ЛНКС. Том. 510. Спрингер. стр. 148–164 . Проверено 29 июня 2013 г.

См. также

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