1. Создание таблиц и форм для ввода и хранения списков (1 занятие).

2. Реализация алгоритмов преобразования описания списка в машинное представление и обратно (2 занятия).

3. Реализация операций над списками (2 занятия)

4. Реализация алгоритма Eval (2 занятия).

5. Оформление результатов (1 занятие).

4. Логическое программирование

Логическое программирование основывается на представлении задач в виде теорем, доказываемых в рамках исчисления предикатов первого порядка.

4.1Модели и опровержения

В доказательстве теорем стараются показать, что определенная ППФ B есть логическое следствие множества ППП S = {A₁, …, A_n}, называемых аксиомами рассматриваемой задачи. Правило вывод есть правило, при помощи которого из ранее полученных выражений можно получить новое. Например, если A_iи A_jистинные ППФ, то запись:

указывает, что A_k можно получить из A_iи A_j с помощью правила f_q. Рассмотрим последовательность S(0), …, S(j+1), образованную из некоторого множества аксиом S по правилу:

S(0) = S,

…

S(j+1) = S(j) È F(S(j),

где F(S) – множество выражений, которое можно получить из множества S, применяя к каждому его элементу все возможные правила f_qиз конечного множества F={f_q}. Говорят, что высказывание Bследует из аксиом, принадлежащих S, если BÎS(j) для некоторого j.

Напомним, что терм – это константа, переменная или функция. В качестве своих аргументов n – местная функция должна иметь п термов. Таким образом, термами будут: a, b, c, f(a), g(f(x), y).

Атомом называется предикат со своими аргументами. Литерал – это атом или его отрицание. Предложение C – это дизъюнкция литералов. Множество предложений Sинтерпретируется как единое высказывание, представляющее конъюнкцию всех его предложений.

Как уже отмечалось, высказывание Tследует из множества предложений S, если T есть логическое следствие предложений из S. Предположим для простоты, что T состоит из единственного предложения. Рассмотрим множество предложений:

Для того, чтобы высказывания SÈTбыли истинными, все предложения C_iи T должны быть истинными. В свою очередь значения истинности этих предложений будут определяться значениями истинности, содержащихся в них атомов, причем значения истинности должны присваиваться атомам так, чтобы, по крайней мере, один литерал в каждом предложении был истинным.

Отдельное присваивание истинности атомам называется моделью. Если Sвлечет за собой T, то не существует модели, в которой Sистинное, а T– нет. Вместе с тем, если высказывание Tистинное, то его отрицание должно быть ложным. Поэтому, если Sвлечет за собой T, высказывание:

(1)

должно быть ложным для любой модели.

Этот же вывод можно сделать следующим образом:

и от противного:

Предположим, что число атомов конечно. Тогда существует конечное множество моделей, так как k атомам можно присвоить логические значения 2^kразличными способами. Очевидно, что присваивать значения этим комбинациям можно последовательно и если для всех моделей (1) окажется ложным, то, безусловно, Sвлечет T. Такое доказательство называется методом от противного и составляет основу методов доказательства теорем.

Доказать противоречивость (1), если число атомов конечно, достаточно просто. Просто ли это на практике зависит от количества атомов и от возможности порождать и проверять модели.

Возникает задача выявления условий, гарантирующих конечное число атомов. Пусть S– это множество высказываний истинных для тех атомов, которые непосредственно входят в Sи тех, которые из них можно вывести. Последнее множество может быть бесконечным. В этом можно убедиться на следующем примере. Пусть S– высказывание, содержащее единственный атом S = {R(a, x)}.

Предположим, что определена функция g(x). Тогда можем построить бесконечную последовательность R(a, x), R(a, g(x)), R(a, g(g(x))), … . Эта последовательность перечислимая, так как можно придумать схему перечисления, по которой упорядочиваются высказывания. Например, по уровню вложенности второго аргумента. Можно показать, что всегда можно построить схему перечисления бесконечного множества атомов, полученного из конечного при помощи некоторой подстановки.

Предположим, что Sне содержит переменных. Такая ситуация называется основным случаем, а соответствующий универсум (область определения) Эрбрановой базой. В основном случае можно провести перечисление.

Докажем, например, для конкретной пары чисел (a, b) (но не для произвольной пары чисел вообще x, y) истинность высказывания:

a = b ® a > b.

Аксиомами будут:

A1: a > b,

A2: a < b,

A3: a = b.

Соответствующие предложения будут иметь вид:

- выполняется одно из отношений;

- одновременно не выполняются никакие два отношения.

В этих обозначениях наше утверждение имеет вид:

и его отрицание A3A1. Отсюда получим:

Обозначим

Так как в Sможет быть только 2³ = 8 атомарных высказываний, легко построить все возможные модели. Если для каждой из них хотя бы одно предложение в Sпринимает значение ложь, то высказывание вида (1) будет ложным, и поэтому наше утверждение будет истинным.

Модель	Предложения, которым присваивается значение ложь
A1, A2, A3	C2, C3, C4

	C3

Этот метод неэффективен и избыточен. Можно показать, что высказывание S противоречиво, если исследовать меньшее число моделей. Достаточно ограничиться атомами A1 и A3, то есть провести присваивание значений истинности только этим атомам, а значит использовать только четыре модели.

Теорема Эрбрана – Сколема – Геделя. В этой теореме утверждается, что можно найти частичное присваивание, приписывающее значение ложь любому противоречивому множеству предложений.

4.2 Доказательство от противного

4.2.1Неаксиоматическое описание процедуры

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

Пусть в качестве åзадана группа логических формул следующего вида:

Отец(x, y) : x является отцом y;

Брат(x, y) : x, y – братья;

Кузен(x, y) : x, y – двоюродные братья;

Логическое и функциональное программирование (стр. 12 из 16)

4. Логическое программирование