Оглавление:
Определение - Что означает Объединение?
В информатике и логике унификация - это алгоритмическая процедура, используемая при решении уравнений с символическими выражениями. Другими словами, заменяя некоторые переменные подвыражения другими выражениями, объединение пытается идентифицировать два символических выражения. Унификация используется в технологии автоматизированного рассуждения, которая остается одной из основных областей применения унификации.
Унификация используется в таких реализациях, как:
- Реализация системы языкового типа программирования
- Логическое программирование
- SMT решатели
- Анализ криптографического протокола
- Алгоритмы переписывания терминов
Унификация является одним из фундаментальных методов, на которых основаны методы автоматического вывода.
Техопедия объясняет объединение
Термин «объединение» и его понятие можно отнести к Джону Алану Робинсону. Он использовал объединение в качестве основной операции своего принципа разрешения, а также показал, что унифицируемые термины имеют не более одного общего объединителя. Несколько рамок объединения дифференцируются на основе выражений, которые встречаются в проблеме объединения. Объединение первого порядка - это то, в котором переменные высшего порядка (переменные, представляющие функции) разрешены в выражениях. Свободное объединение или синтаксическое объединение - это то, в котором необходимо решение, чтобы обе стороны уравнения были равны.
Решение проблемы объединения изображается путем подстановки, которая представляет собой отображение символического значения на каждую переменную, участвующую в выражениях задачи. Другими словами, основной целью объединения является поиск замены, чтобы объединить два заданных термина. Ожидается, что более унифицированный алгоритм обеспечит минимальный и полный набор подстановок (набор, имеющий все соответствующие решения без лишних членов) для данной проблемы. Другими словами, объединение заинтересовано не только в разрешимости данного объединения, если оно существует, но и в том случае, если оно решаемо, в вычислении наиболее общего объединителя.
Объединение считается ядром:
- Пролог реализации
- Экспертные системы на основе искусственного интеллекта
- Сопоставление с образцом в функциональных языках
- Определенные подходы разбора
- Дедуктивные базы данных
- Обработка естественного языка
- Доказательство теорем
- Алгоритмы вывода типов
