Оглавление
Разрешение SLD
-
Основы логического программирования
- Логическое программирование – это формальное программирование, использующее логику для описания вычислений.
- Логические программы состоят из набора предложений, которые могут быть истинными или ложными.
- Логическое программирование отличается от традиционного программирования, где программы состоят из последовательности инструкций.
-
SLD-разрешение
- SLD-разрешение – это метод доказательства разрешения, который позволяет опровергать предложения.
- SLD-разрешение использует линейную последовательность предложений, где последнее предложение может быть пустым.
- В SLD-разрешении функция выбора позволяет выбрать литерал из предложения.
-
Вычислительная интерпретация SLD-разрешения
- SLD-разрешение демонстрирует, что входной набор предложений не является удовлетворительным.
- В логическом программировании SLD-разрешение имеет вычислительную интерпретацию, где главное предложение представляет собой отрицание совокупности подцелей.
-
Стратегии разрешения споров в SLD
- SLD-разрешение не определяет стратегию поиска, что делает его недетерминированным.
- Prolog использует поиск в глубину, но может быть неполным из-за бесконечных ветвей.
- Существуют различные стратегии поиска, включая последовательный и параллельный поиск.
-
SLDNF
- SLDNF – это расширение SLD-разрешения, которое рассматривает отрицание как неудачу.
- SLDNF позволяет рассматривать отрицание в виде литералов отказа, которые могут быть выбраны только без переменных.
-
Рекомендации
- Ссылки на работы Роберта Ковальски и Дональда Кюнера, а также на статью Жана Галье.
- Упоминание о внешних ссылках для дополнительной информации.