Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АрхитектураБиологияГеографияДругоеИностранные языки
ИнформатикаИсторияКультураЛитератураМатематика
МедицинаМеханикаОбразованиеОхрана трудаПедагогика
ПолитикаПравоПрограммированиеПсихологияРелигия
СоциологияСпортСтроительствоФизикаФилософия
ФинансыХимияЭкологияЭкономикаЭлектроника

Процедура вывода решения, как процедура доказательства теоремы

Основные задачи для функционального и логического программирования. | Основные примитивы Лиспа для обработки списка. | Рекурсия по аргументу, пример | Косвенная рекурсия, пример | Реализация рекурсивного вызова, функция трассировки в Лиспе | Применяющий функционал Лиспа | Генератор в программировании, понятие вычислительного контекста | Теория Тьюринга, значение для логического программирования. | Сопоставление в логическом программировании | Запись списка в виде структуры |


Читайте также:
  1. III. Процедура защиты выпускной квалификационной работы в Государственной аттестационной комиссии
  2. IV. Заполнение ДТ при декларировании товаров Таможенного союза в таможенных процедурах СТЗ или свободного склада
  3. V. ПРОЦЕДУРА РАССМОТРЕНИЯ И КРИТЕРИИ ОЦЕНКИ ЗАЯВОК
  4. VI. Особенности заполнения ДТ в таможенных процедурах реэкспорта или экспорта при завершении действия таможенных процедур СТЗ и свободного склада для отдельных категорий товаров
  5. VI. Процедура защиты выпускной квалификационной работы
  6. Асимметрия вывода на основе экспериментальных данных
  7. В каком порядке осуществляется процедура санкционирования?

Логическое программирование - программирование, основанное на механизме доказательства теорем в логике. Теоремы описывают предметную область, а программа состоит из набора аксиом, описывающих предметную область и теоремы, которую необходимо доказать. Доказательство осуществляется методом резолюции.

Метод резолюции формируется следующим образом: если выводимые атомарные формулы (p || q) и (!p || R) то выводимы следующие формулы (Q || R), где p - заголовок атомарной формулы, Q и R - остальная часть формулы, возможно включающая комбинацию из других формул. (Q || R) - дизьюнктор (резолюция).

Процедура логического вывода, основанного на резолюция заключается в следующем: 1) к фразам, описывающих предметную область, добавляется отрицание теоремы. 2) выполняется поиск аксиомы, с которой может быть выполнена резолюция в простом линейном порядке. 3) При нахождении такой аксиомы, к применяется резолюция, и она добавляется во множество аксиом, описывающих предметную область. Эта процедура повторяется до тех пор, пока не будет получен пустой дизьюнкт.

Пустым дизьюнктом называется дизьюнкт следующего вида (p &&!p)

В процессе доказательства выполняются унификации атомарных формул, при этом возможна конкретизация переменных. Унификация проходит успешно, если совпадают предикатные имена, состовляющих формул и арности.

 


Дата добавления: 2015-07-19; просмотров: 73 | Нарушение авторских прав


<== предыдущая страница | следующая страница ==>
Переменная, конкретизация переменных| Определение оператора и его свойства.

mybiblioteka.su - 2015-2024 год. (0.006 сек.)