Алгебра логики
<<  Функциональное и логическое программирование Развитие логического мышления в процессе обучения младших школьников  >>
Логическое программирование
Логическое программирование
Дизъюнкция и ложь
Дизъюнкция и ложь
Нормальная форма программ
Нормальная форма программ
Приведение к нормальной форме
Приведение к нормальной форме
ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (продолжение)
ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (продолжение)
ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (окончание)
ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (окончание)
Равенство
Равенство
Явный бэктрекинг
Явный бэктрекинг
Правила для конъюнкции и истины
Правила для конъюнкции и истины
Правила для атомарных предикатов
Правила для атомарных предикатов
Правила для дизъюнкции
Правила для дизъюнкции
Корректные правила дизъюнкции
Корректные правила дизъюнкции
Правила для равенства
Правила для равенства
Явность
Явность
Явность
Явность
Явность
Явность
Явность
Явность
Явность
Явность
Явность
Явность
Завершенность
Завершенность
Метаинтерпретатор для явного бэктрекинга
Метаинтерпретатор для явного бэктрекинга
Метаинтерпретатор для явного бэктрекинга
Метаинтерпретатор для явного бэктрекинга
Абстрактные машины
Абстрактные машины
Основные понятия на сегодня
Основные понятия на сегодня
Логическое программирование
Логическое программирование
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Унификация и поиск доказательств
Подстановки
Подстановки
Подстановки
Подстановки
Подстановки
Подстановки
Композиция подстановок
Композиция подстановок
Композиция подстановок
Композиция подстановок
Композиция подстановок
Композиция подстановок
Композиция подстановок
Композиция подстановок
Унификация
Унификация
Унификация
Унификация
Унификация
Унификация
Унификация
Унификация
Явность
Явность
Основные понятия на сегодня
Основные понятия на сегодня

Презентация: «Логическое программирование». Автор: Igor. Файл: «Логическое программирование.ppt». Размер zip-архива: 227 КБ.

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

содержание презентации «Логическое программирование.ppt»
СлайдТекст
1 Логическое программирование

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

Бэктрекинг

1

2 Дизъюнкция и ложь

Дизъюнкция и ложь

Попытаемся сделать выбора правил явным. Для этого введем новые связки: дизъюнкцию и ложь Ложь это дизъюнкции нулевых альтернатив

2

3 Нормальная форма программ

Нормальная форма программ

Явная конъюнкция в программе – если каждое продукционное правило имеет в точности одну предпосылку. Но возможны несколько правил для одной цели. Тогда следует привести программу к нормальной форме. Нормальная форма программ = программа в явной дизъюнктивной форме. В таком случае каждая цель соответствует голове в точности одного правила.

3

4 Приведение к нормальной форме

Приведение к нормальной форме

Это не явная дизъюнктивная форма потому что: Нет утверждения для member(t, []) Для целей member(t, [t | ys]) могут быть применены оба утверждения

4

5 ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (продолжение)

ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (продолжение)

Теперь оба правила имеют одинаковый консеквент. Объединяем их дизъюнкцией:

5

6 ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (окончание)

ПРИВЕДЕНИЕ К НОРМАЛЬНОЙ ФОРМЕ (окончание)

Теперь добавим утверждение для отсутствующего случая, с предпосылкой ложь Программа приведена в явную дизъюнктивную форму с предположением, что второй аргумент – список. На Прологе: member(X, []) :- fail. member(X, [Y | Ys]) :- X = Y ; member(X, Ys).

6

7 Равенство

Равенство

Вводное правило для высказывания , означающего, что s и t равны: Мы также можем использовать s ? t, чтобы указать, что два терма различны, в качестве вида рассуждения

7

8 Явный бэктрекинг

Явный бэктрекинг

Программа представлена в дизъюнктивной нормальной форме. Главный выбор – доказать A?B в качестве цели. Операционная семантика Пролога: сначала решить A и только если решение завершится неудачей, решить B. К стеку цели S, мы добавляем другой аргумент F, который хранит дальнейшие (неиспользованные) возможности. F – продолжение неудачи (failure continuation). Записываем новое рассуждение как A / S / F и читаем его так: Или А при S или F. Формально : If A / S / F then (A?S) ? F true.

8

9 Правила для конъюнкции и истины

Правила для конъюнкции и истины

Они не меняются сильно, а только обеспечивают продолжение неудачи

9

10 Правила для атомарных предикатов

Правила для атомарных предикатов

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

10

11 Правила для дизъюнкции

Правила для дизъюнкции

Доказательство: методом индукции на структуре дедукции для A / S / F. Мы должны показать, что если (A ? S)? (B ? F) истина, то ((A ? B) ? S) ? F истина. Раскрываем скобки: или A ? S истина, или В истина, или F истина. В среднем случае недостаточно информации, чтобы заключить, что ((A ? B) ? S) ? F истина. Доказательство невозможно.

11

12 Корректные правила дизъюнкции

Корректные правила дизъюнкции

Мы должны объединить попарно альтернативу В со стеком цели S и восстановить S, когда мы делаем бэктрек, рассматривая В. Стек цели S’ во втором правиле отбрасывается, поскольку применяется к цели , которая не может быть успешной. Вместо этого мы восстанавливаем стек цели S, сохраненный с В. Здесь остался один случай, который не покрыт правилами: нет правила для . Общая цель терпит неудачу, если текущая цель неудачна, и здесь нет дальнейших альтернатив.

12

13 Правила для равенства

Правила для равенства

В Прологе сложностей не вызывают. Мы всегда можем сказать, равны два терма или нет.

13

14 Явность

Явность

Теорема. Если A / S / F то (A ?S)? F истина. Доказательство: С помощью индукции на структуре D A / S / F.

14

15 Явность

Явность

Случай 1: истина из гипотезы из инверсии первая часть дизъюнкции из двух инверсий из двух применений правила из правила ( ) F истина вторая часть дизъюнкции из правила ( )

15

16 Явность

Явность

Случай 2: Аналогичен предыдущему случаю. Случай 3: из правила ( ) из правила ( ) из правила ( )

16

17 Явность

Явность

Случай 4: (B?S)?F истина гипотеза из D’ B истина и S истина первый подслучай после инверсии P истина из правила (P?S)?F истина из правил (?I и ?I1) F истина второй подслучай после инверсии (P?S)?F истина из правила (?I2)

17

18 Явность

Явность

Случай 5: (A1 ?S)? ( (A2?S) ?F) из гипотезы в D1 A1 истина и S истина первый подслучай после инверсии A1 ? A2 истина из правила (?I1) ((A1 ? A2) ?S) ?F) из правил (?I и ?I1) A2 истина и S истина второй подслучай после инверсии A1 ? A2 истина из правила (?I2) ((A1 ? A2) ?S) ?F) из правил (?I и ?I1) F истина третий подслучай после инверсии ((A1 ? A2) ?S) ?F) из правила (?I2)

18

19 Явность

Явность

Случай 6: (A2 ? S1)?F0 истина из гипотезы D2 (?S)?((A2?S1) ? F0) истина из правила (?I2) Остальные случаи: Докажите дома

19

20 Завершенность

Завершенность

Данный набор правил не является завершенным. Например, такое правило Не может быть найдено с помощью поиска, поскольку нет доказательства даже если есть простое доказательство, что diverge истина:

20

21 Метаинтерпретатор для явного бэктрекинга

Метаинтерпретатор для явного бэктрекинга

True, true, _, istrue). Solve(true, (A , S), F, J) :- solve(a, S, F, J). Solve((a,b), S, F, J) :- solve(a, (B, S), F, J). Solve(fail, _, fail, isfalse). Solve(fail,_,((b,s) ; F), J) :- solve(b,s,f,j). Solve((a ; B),S,F,J):- solve(a,s,((b,s) ; F), J). Solve((x = Y),S,F,J) :- X = Y, solve(true,s,f,j). Solve((x = Y),S,F,J) :- X \= Y, solve(fail,s,f,j). Solve(p,s,f,j) :- clause(p,b), solve(b, S, F, J). % Интерфейс верхнего уровня solve(a, J) :- solve(a, true, fail, J).

21

22 Метаинтерпретатор для явного бэктрекинга

Метаинтерпретатор для явного бэктрекинга

Имея программу в явной дизъюнктивной форме, такую, как member(X, []) :- fail. member(X, [Y|Ys]) :- X = Y ; member(X, Ys). мы можем задать цель: ?- solve(member(1, [2,3,4]), J). J = isfalse; ?- solve(member(1, [1,2,1,4]), J). J = istrue; Каждый запрос будет завершаться успехом только один раз, поскольку наш метаинтерпретатор находит только первое решение.

22

23 Абстрактные машины

Абстрактные машины

Анализируя правила, мы можем видеть, что для каждого состояния имеется уникальное преобразование состояния, за исключением: Состояние является финальным, поскольку не существует предпосылок, удовлетворяющих правилу. Вычисление завершается. Состояние является финальным, поскольку нет правил, которые можно применить. Вычисление заканчивается неудачей. Состояние P/S/F вызывает уникальное преобразование (в соответствии с требованием, что естm уникальное правило для каждой атомарной цели P), правда, как найти экземпляр правила, остается неформальным.

23

24 Основные понятия на сегодня

Основные понятия на сегодня

Нормальная форма программ Явный бэктрекинг Явность Завершенность Абстрактные машины

24

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

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

Унификация

25

26 Унификация и поиск доказательств

Унификация и поиск доказательств

Пусть есть унарное сложение И атомарная цель plus(p(0), p(p(0)), S). Только консеквент второго правила соответствует цели. На какой вопрос мы должны ответить, чтобы прийти к этому утверждению?

26

27 Унификация и поиск доказательств

Унификация и поиск доказательств

«Имеется такой экземпляр правила, что его консеквент удовлетворяет цели». Мы можем видеть, что эта спецификация не вполне верна: нам необходимо конкретизировать также и цель, поскольку S должно иметь форму p(S1) для пока еще неизвестного S1. Подцель в таком случае должна быть plus(0, p(p(0)), S1) в соответствии с конкретизаций правила 0 для M, p(p(0)) для N и S1 для S.

27

28 Унификация и поиск доказательств

Унификация и поиск доказательств

«Существует экземпляр правила и экземпляр цели такие, что они равны». Данная формулировка также несостоятельна. Например, подстановка p(p(p(p(0)))) для S в цели и S в правиле вместе с подстановкой для M и N, как в предыдущем варианте, будет также делать цель и консеквент правила идентичными, но это абсолютно неверно. Проблема в том, что здесь заявляется больше, чем может быть сделано: использование S1 для S в правиле, с другой стороны, оставляет переменную свободной. S1 будет детерминировано позже при поиске и других унификациях. Чтобы обозначить это, определяем, что t1 более общее, чем t2, если t1 может быть конкретизировано в t2.

28

29 Унификация и поиск доказательств

Унификация и поиск доказательств

«Найти более общий экземпляр правила и цели такие, что консеквент правила равен конкретизированной цели». В терминах подстановок это звучит так: найти ?1 и ?2 такие, что S’?1 = S?2, а любой другой экземпляр S’ и S это экземпляр S’?1.

29

30 Унификация и поиск доказательств

Унификация и поиск доказательств

«Сначала переименуем переменные в правиле таким образом, что они будут отличаться от переменных в цели. Затем найдем одну, наиболее общую подстановку ?, которая унифицирует переименованный консеквент с целью». Здесь унификация подстановки ? является наиболее общей, если любая другая унифицирующая подстановка является экземпляром ?.

30

31 Подстановки

Подстановки

Подстановки ? ::= t1/x1,…,tn/xn Мы постулируем, что все xi уникальны. Порядок следования пар в постановках безразличен, и мы считаем перестановки подстановок равными. Мы обозначаем доменом (domain) от ? dom(?)={ x1,…,xn}. Похожим образом мы называем множество переменных, встречающихся в выражении подстановки ti, со-доменом (со-domain) в виде .

31

32 Подстановки

Подстановки

Допущение: Все подстановки допустимы (valid), что означает dom(?)?cod(?) = ? для любой подстановки ?. Это по большому счету единственный способ выполнения. Более общее допущение – это то, что все подстановки идемпотентны (идемпотентность – свойство объекта, состоящее в том, что любые действия над объектом не изменяют его), но мы верим, что вышеописанное более удобно для наших ограниченных целей.

32

33 Подстановки

Подстановки

Применение подстановки ? к выражению t можно достаточно просто определить композиционно: x? = t если t/x в ? y? = y если f(t1,…,tn) ? = f(t1 ?,…,tn ?)

33

34 Композиция подстановок

Композиция подстановок

Общее решение состоит в композиции этих двух подстановок. Мы записываем это как ??. Главное свойство, которое нам нужно: для любого t имеем (t?)?=t(??). Чтобы это свойство могло поддерживать наши общие допущения о подстановках, мы специфицируем предусловие, что dom(?)?dom(?) = ?. Мы определяем композицию как подстановки слева направо, пока не встретим пустую подстановку (.). (t/x, ?) ? = t?/x, ?? (.) = ?

34

35 Композиция подстановок

Композиция подстановок

Теорема (композиция подстановок). Допустим, у нас есть выражение t и допустимые подстановки ? и ? при dom(?) ?dom(?)= ? и dom(?) ?cod(?)= ?. Тогда ?? допустимая подстановка и (??)? = t(??) Более того, если ? это подстановка, такая, что dom(?) ?dom(?)= dom(?) ?dom(?)= ?, то также (??)? = ?(??) Доказательство: Допустимость ?? уже была показана выше. Первое равенство следует из индукции на структуре выражения t, второе – из индукции на структуре ?.

35

36 Композиция подстановок

Композиция подстановок

Случай 1: t=x для переменной x. Тогда мы различаем два подслучая. Подслучай: x dom(?) где s/x?. (x?)? = s? по определению x? = x(??) поскольку s?/x ?? Подслучай: x dom(?). (x?)? = x? по определению x? = x(??) по определению ??

36

37 Композиция подстановок

Композиция подстановок

Случай 2: t=f(t1,…,tn) для выражений t1,…,tn. (t?)? = f(t1?,…,tn) для выражений t1,…,tn по определению t? = f((t1?)?,…,(tn?)?) по определению f(_)? = f((t1(??),…,(tn (??)) и т.д. n раз =f(t1,…,tn)(??)=t(??) по определению t(??)

37

38 Унификация

Унификация

Допустим ? это унификатор t и s, если t?=s?. Мы говорим, что ? это наиболее общий унификатор для t и s, если он является унификатором, а для любого другого унификатора ? существует подстановка ?’ такая, что ? = ??’. Другими словами, унификатор является наиболее общим, если любой другой унификатор является его экземпляром, где «экземпляр» это композиция подстановок.

38

39 Унификация

Унификация

Рассуждение имеет форму t s | ?, где t и s – входы, а наиболее общий унификатор ? – выход. Чтобы обойти n- арную природу списка аргументов, мы будем иметь внешнее рассуждение t s | ? для последовательностей выражений t и s Применение подстановок может расширяться до последовательности выражений очевидным способом. Мы используем (.) в качестве пустой последовательности выражений (а также для пустой подстановки, являющейся последовательностью выражений и пар переменных)..

39

40 Унификация

Унификация

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

40

41 Унификация

Унификация

Условие, что t = f(t) в последнем правиле гарантирует, что оно не пересекается с правилом для x t. Условие, что x FV(t) необходимо потому, что, например, два выражения x и f(x) не имеют унификатора: неважно, что подстановка f(x)? всегда имеет на одно появление f больше, чем x?, и поэтому они не могут быть равными. Другая ситуация, когда унификация терпит неудачу – это уравнение в форме f(t) = g(s) для f ? g, и две последовательности выражений имеют разную длину. Последнее может случиться, если функции имеют разную арность, и в таком случае неудача унификации это корректный результат.

41

42 Явность

Явность

Теорема. Если t s | ? то t? = s?. Доказательство: Нам нужно обобщить это, чтобы покрыть рассуждение внешней унификации на последовательности выражений. Если t s | ? то t? = s?. Если t s | ? то t? = s?. Доказательство выполняется с помощью взаимной индукции на структуре дедукции D от t s и E от t s. Это означает, что если одно рассуждение появляется в качестве предпосылки правила для другого, мы можем применить подходящую гипотезу индукции.

42

43 Основные понятия на сегодня

Основные понятия на сегодня

Унификация Подстановки Композиция подстановок Явность

43

«Логическое программирование»
http://900igr.net/prezentacija/algebra/logicheskoe-programmirovanie-135152.html
cсылка на страницу

Алгебра логики

19 презентаций об алгебре логики
Урок

Алгебра

35 тем
Слайды
900igr.net > Презентации по алгебре > Алгебра логики > Логическое программирование