Общая схема построения формальной системы.

1) Определение языка системы. Здесь определяется алфавит (перечень элементарных символов системы), правила построения формул (синтаксис высказывания).

2) Определение аксиом системы. Здесь выделяется конечное или перечислимое множество формул, которые называют аксиомами. Аксиомы – это утверждения, заведомо истинные и не требующие доказательства.

3) Определение правил вывода системы. Фиксируется множество предикатов R_i, i >0 на множестве всех формул. Если для некоторого набора формул F₁, F₂, …, F_n истин предикат R_i(F₁,.., F_n+1), то говорят, что формула F_n+1 непосредственно вытекает из формул F₁ … F_n по правилу F_i.

Задание языка, аксиом, правил вывода обеспечивает задание формальной системы.

Теорема системы – это некоторая формула, выводимая на заданном множестве формул, аксиом системы.

Выводом в формальной системе называется любая последовательная конечность формул, в которой каждая формула является либо аксиомой, либо следствием из каких-либо последовательных формул по одной из правил R_i.

Вывод форм S в некоторой системе Т представляется следующим образом:

F₁, F₂, …, F_n\_Т F

Пример 5.1

Задача раскроя материала.

Имеется 2 вида материала:

M₁, L₁ = 100 см;

M₂, L₂ = 120 см.

Изделие, которое нужно получить, имеет длины n₁ = 80 см, n₂ = 60 см, n₃ = 30 см.

Состояния, в которых находится система, задаются предикатом:

S(m₁, m₂, n₁, n₂, n₃).

Начальное состояние системы S(m₁, m₂, 0, 0, 0).

Правила вывода:

1) S(x+1, y, z, u, v) + S(x, y, z+1, u, v).

2) S(x+1, y, z, u, v) + S(x, y, z, u+1, v+1).

3) S(x+1, y, z, u, v) – S(x, y, z, u, v+3).

4) S(x, y+1, z, u, v) – S(x, y, z+1, u, v+1).

5) S(x, y+1, z, u, v) + S(x, y, z, u+1, v+2).

6) S(x, y+1, z, u, v) + S(x, y, z, u+2, v).

7) S(x, y+1, z, u, v) + S(x, y, z, u, v+4).

Это – моделирование в виде исчисляемой системы, находящейся на каждом шаге в некотором состоянии, из которого она может перейти по одному из правил в следующее состояние. Процесс перехода является недетерминированным.

 

Основные понятия логического программирования.

Предикат – это отношение между объектами.

Атом – это имя конкретного объекта.

Логическая переменная обозначает неопределенные объекты. С помощью логических переменных можно определить в программах структуру логических данных, называемых термами. При этом терм может быть константой, переменной, либо составной структурой. Структура содержит функтор – последовательность из одного или более элементов, являющихся термами. Функтор задается именем и числом аргументов:

f(t₁, …,t_n); t/n.

Примеры структур:

S(0).

not(milk).

name(john, dough).

foot(X).

list (a, list, (b, nd)).

tree(tree nd, 3, nit, 3, R).

вопросы, цели и термы, не содержащие переменных, называются основными. Термы, содержащие переменные, называются не основными.

Подстановкой называется некоторое множество пар вида: x_i = t_j, причем x_i не входит в t_j,

x_i ¹ t_j, " i и j,

x_i ¹ x_j, i ¹ j.

Пример подстановки, состоящий из одной пары: X = milk.

Подстановка может применяться к термам. Результат применения подстановки Q к некоторому терму А обозначается QA и представляет собой терм, полученный заменой каждого вхождения некоторой переменной x терма A на значение терма t для каждой пары (" x = t в Q).

 

Терм А называется примером В, если существует такая подстановка Q, что A = QB.

Например, цель:

like(john, wine).

like(john, X).

 

sister(pat, list).

sister(X, Y).

В логических термах переменные-вопросы связаны квантором существования.

Универсальные факты содержат переменные-утверждения (Все любят цветы):

like(X, flowers).

mult(0, X, 0).

Из универсальных фактов можно вывести любой пример факта. Правило вывода называется конкретизацией.

Общим примером термов А и В называется терм С, если он является примером А и примером В одновременно, т.е. существуют такое подстановки E = AQ₁ = BQ_2.

Например, 2 терма:

add (0, Y, 3) Q₁ = 3.

add (0, X, X) Q₂ = 3.

Общим при поиске ответов на вопрос с использованием факта лежит общий пример вопроса и факта. Если такой пример существует, то он является ответом на вопрос. Составные вопросы являются конъюнкцией.

? – Q₁, Q₂, …, Q_n.

Если каждая цель в вопросе независима, то ответ на вопрос – «да», если каждая цель выводится из программы, т.е. является следствием состояния, представленным вопросом, в котором существует одна или более общих переменных для разных целей:

? – p(x), q(x).

Эту запись интерпретируется следующим образом: Существует ли такое x, что истинны цели p(x), q(x) одновременно?

Переменные в составных вопросах связаны квантором существования. Общая переменная в этом случае используется для сокращения пространственного поиска значений переменных.

Правилом называется утверждение вида АВ₁, …, B_n при n > 0.

Факт является частным случаем правила при n < 0. При n = 1 получаем рекурсию. В правилах переменные связаны квантором общности А, при этом область действия распространяется на все правила:

сын(X, Y) отец(Y, X), мужчина(X).

дочь(X, Y) отец(Y, X), женщина(X).

дед(X, Z) отец(Y, X), отец(Y, Z).

Возможны 2 варианта интерпретации правил:

1) Процедурный. Для ответа на вопрос: «Является ли некто X дедом Z?», - необходимо последовательно доказать истинность утверждения, что X является отцом Y, а Y является отцом Z.

2) Декларативный. С этой точки зрения правило истолковывается как логическая аксиома " X, Y, Z. Если X – отец Y и Y – отец Z, то X – отец Y и Y – отец Z, тогда X – дед Z.

Для рассмотрения процедуры логического вывода используется закон, который в логике называется modus pones.

Из некоторого правила R = (AB₁, …, B_n) и фактов B’₁, …, B’_n выводится следствие А, если оно является примером правила R.

Логическая программа Р – конечное множество правил.

Некоторая цель G с кванторами является логическим следствием программы Р, если в программе найдется такое предпочтение с основным примером: A B₁, …, B_n, и B_i, 1 < i < n, что высказывания B_i являются следствием программы, а следствие А является примером цели G.

Примечание: Цель в логике – программа существует, когда она может быть выведена с помощью конечного числа применений правила modus pones.

Процедура поиска ответа на вопрос отражает определенные логические следствия. Здесь угадывается основной пример цели и правила, затем рекурсивно ищется ответ на составной вопрос, соответствующий телу правила. Доказательство некоторой цели А в программе Р сводится к поиску правила: A_iB_i, …, B_n и указанию такой подстановки Q, что цель определяется как A = A_iQ, а В_iQ – являются основными целями.

Затем рекурсивно доказывается каждая составная цель в порядке указания логической программы, которая может включать альтернативные определения одних и тех же термов, что формально эквивалентно дизъюнкции.

Например:

родитель(X, Y) отец(X, Y).

родитель(X, X) мать(X, Y).

родитель(X, Y) отец(X, Y) or мать(X, Y).

Указанная совокупность правил с одинаковым именем предиката называется процедурой.