Технологии ИИ1 ТЕХНОЛОГИИ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА Лекция 2. Формальные системы. - презентация

1 Технологии ИИ1 ТЕХНОЛОГИИ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА Лекция 2. Формальные системы

2 Технологии ИИ2 Определения Формальная система (ФС) определяется как четверка ФС = {, F, A, P}, где - конечный алфавит (конечное множество символов, словарь). F - процедура построения формул (слов) формальной системы (грамматика формул). Можно трактовать как определение того, что такое формула. A - конечное множество формул, называемых аксиомами. P - конечное множество правил вывода, которые позволяют получать из некоторого конечного множества формул другое множество формул: U 1, U 2,…,U n W 1, W 2,…W m U i, W i – формулы ФС.

3 Технологии ИИ3 Определения Определение. Формальное доказательство – это конечная последовательность формул M 1, M 2, …, M r таких, что каждое M i – либо аксиома, либо M i выводима при помощи одного из правил вывода из предшествующих формул M j, j

4 Технологии ИИ4 Исчисление высказываний Примером ФС является исчисление высказываний (ИВ). ИВ – это ФС, называемая также логикой высказываний (пропозициональной логикой). Алфавит ИВ: Пропозициональные буквы p, q, r, s, t, … Логические операторы (не), (влечет, следует) Скобки '(, ). Построение формул ИВ: Любая пропозициональная буква суть формула. Если m-формула, то и (m) является формулой. Если m-формула, то m является формулой. Если m1 и m2 – формулы, то m1 m2 – формула. Аксиомы ИВ: (A1): m1 (m2 m1) (A2): (m1 (m2 m3)) ((m1 m2) (m1 m3)) (A3): ( m2 m1) (m1 m2) Правила вывода: m1 и (m1 m2) | m2 (modus ponens или правило отделения) В этой ФС 3 закона логики Аристотеля являются строго доказуемыми: Закон тождества: (p p) Закон исключения третьего: (p p) Закон противоречия: ( (p p)) Введение новых символов: (И): m1 m2 ( m1 m2) (ИЛИ): m1 m2 ( m1 m2) (ТОЖДЕСТВО): m1 m2 (m1 m2) (m2 m1) Если истинно и истинно, что из следует, то также будет истинным. «Каждый человек смертен. Сократ человек. Следовательно, Сократ смертен». (modus Barbara, т.к. здесь имеются кванторы всеобщности).

5 Технологии ИИ5 Множество ИВ Можно построить множество различных систем аксиом ИВ. В том числе, возможно уменьшение числа аксиом и количества операторов: Оператор - т.н. штрих Шеффера и одна аксиома. Штрих Шеффера определяется следующим образом: p | q ( p) ( q) Аксиома Дж.Нико, 1916: (A|(B|C)) | {[D | (D | D)] | [(E|B| ((A|E) | (A|E))]}

6 Технологии ИИ6 ИВ и теория релейно-контактных схем 1910 г.: Пауль. С. Эренфест ( ): "...Пусть имеется проект схемы проводов автоматической телефонной станции. Надо определить: 1) будет ли она правильно функционировать при любой комбинации, могущей встретиться в ходе деятельности станции; 2) не содержит ли она излишних усложнений. Каждая такая комбинация является посылкой, каждый маленький коммутатор есть логическое "или-или", воплощенное в эбоните и латуни; все вместе - система чисто качественных... "посылок", ничего не оставляющая желать в отношении сложности и запутанности...правда ли, что, несмотря на существование алгебры логики, своего рода "алгебра распределительных схем" должна считаться утопией?" г.: В. И. Шестаков (СССР), К. Шеннон (США) - строгое обоснование возможности использования исчисления высказывании для описания релейно-контактных схем г., монография М.А. Гаврилова ( ) "Теория релейно-контактных схем".

7 Технологии ИИ7 Язык предикатов первого порядка Операции с высказываниями, расчлененными на субъекты и предикаты. Базируется на ИВ. Отсюда следует необходимость понимания внутренней структуры посылок. Появляются кванторы («все», «существует»). Алфавит языка предикатов первого порядка включает в себя: –разделители –константы –переменные –предикаты –функции –логические операторы (,,,, ) –кванторы (, ) Предикат (логическая функция) – это функция от любого числа аргументов, принимающая значения Истина и Ложь. Терм – выражение, включающее константы, переменные и функции. В исчислении предикатов 1-го порядка запрещено квантифицировать символы предикатов и функций. К аксиомам логики предикатов добавляются: x F(x) F(y) F(y) x F(x)

8 Технологии ИИ8 Правильно построенные формулы (ППФ) и предложения Правильно построенная формула (ППФ) –всякий атом есть ППФ –если G и H – ППФ, а X – переменная, то ( H), (G H), (G H), ( X)G, ( X)H – ППФ. Предложение – формула, представляющая собой дизъюнкцию литералов Преобразование ППФ в предложения Исключение символов эквивалентности и импликации F G (F G) (G F) F G F G Уменьшение области действия знаков отрицания. Отрицание должно быть применено не более, чем к одному атому. (F G) F G Разделение переменных. Каждый квантор должен иметь только свою, свойственную ему, переменную. Исключение кванторов существования Например, пусть имеем ( X)( Y) P(X,Y) Видимо, Y зависит от X, т.е. Y=g(X) (т.н. функция Сколема или сколемовская функция). Тогда можно записать: ( X)P(X,g(X))

9 Технологии ИИ9 Принцип резолюции 1930 г. Эрбран. Метод доказательства теорем в ФС первого порядка. Идея: чтобы получить некоторое заключение C, исходя из гипотез H1, H2,…Hn, т.е. доказать теорему T: H1 H2 Hn C, достаточно доказать противоречивость формулы F: H1 H2 Hn C, в которой отрицание заключения добавлено к исходным гипотезам. Это может оказаться проще прямого вывода. Соображения тривиальны: доказательство выполнимости множества G H ( G H) – это опровержение его невыполнимости, т.е. невыполнимости ( G H), что эквивалентно G H. Установление невыполнимости множества предложений осуществляется посредством принципа резолюций – специальной процедуры логического вывода новых предложений из множества исходных.

10 Технологии ИИ10 Резольвенты Пусть имеется два конкретных (не содержащих переменных) предложения P1 P2 … Pn и P1 Q1 … Qm Из этих двух предложений можно вывести новое предложение, называемое резольвентой или резолюцией. Резольвентой является дизъюнкция этих предложений с последующим исключением пары P1 и P1. Очевидно, что принцип резолюций покрывает правило вывода modus ponens. Пример. Пусть имеется пара предложений P R и R Q (или P R, R Q) Резольвентой этих предложений является P Q (или P Q). Это правило вывода называется сцеплением. Для обобщения этого правила на случай предложений, содержащих переменные, используется специальная процедура, называемая унификацией. Пусть имеется пара F(X) G(X) и F(f(Y)) Если первое предложение заменить на F(f(Y)) G(f(Y)), то получим резольвенту G(f(Y)). Унификация заключается в замене переменных с целью появления дополнительных литералов.

11 Технологии ИИ11 Алгоритм опровержения с помощью резолюций Предположим, что целью алгоритма резолюций является доказательства G H. Резолюция(G,H) 1. Сформировать C – множество предложений, полученных путем преобразования формул множества G. 2. Добавить к множеству C предложения, полученные из H. 3. Пока в C не появится пустое предложение выполнять: 3.1. Выбрать 2 различных предложения S1 и S2 из C Если они имеют резольвенту R, то добавить эту резольвенту к множеству C. Конец цикла Конец алгоритма. В этой процедуре требуется предварительное приведение исходных предложений к дизъюнктивной нормальной форме.

12 Технологии ИИ12 Пример 1 Необходимо доказать, что Сократ смертен. Доказательство будем строить на опровержении противоречивости целевого утверждения, т.е. противоречивости Смертен(сократ).

13 Технологии ИИ13 Пример 2 Описание: Любой студент, который сдает экзамен по физике и выигрывает в лотерею – счастлив. Известно, что любой удачливый или старательный студент может сдать все экзамены. Сидоров не относится к числу старательных студентов, но достаточно удачлив. Любой удачливый студент выигрывает в лотерею. Вопрос: счастлив ли Сидоров?

14 Технологии ИИ14 Предикатная и дизъюнктивная формы Предположим, что мы хотим доказать, что Сидоров счастлив. Для этого добавим к нашим выражениям отрицание заключения ("Сидоров счастлив") в дизъюнктивной форме: happy(сидоров).

15 Технологии ИИ15 Граф опровержения Граф опровержения разрешения отражает процесс получения противоречия и, следовательно, доказывает, что Сидоров счастлив

16 Технологии ИИ16 Резолюции в Прологе Пролог основан на логике предикатов первого порядка. В нем используются только предложения Хорна (хорновские дизъюнкты): P 1 P 2 … P n P m или P 1 P 2 … P n P m При этом: резолюция использует первый отрицательный литерал слева направо в центральном предложении резолюции выполняются в глубину, т.е. полученная резольвента тут же участвует в следующей резолюции.

17 Технологии ИИ17 Программа доказательства теорем на основе принципа резолюций Описание исходных предложений: ( a b), ( b c), a, c sent([t(0,"a"),t(1,"b")]). -- ( a b) sent([t(0,"b"),t(1,"c")]). -- ( b c) sent([t(1,"a")]). -- a sent([t(0,"c")]). -- c Здесь 0 - отрицание, 1 - прямая форма Шаг резолюции состоит из следующих действий: Берутся 2 предложения в ДНФ D1 и D2. Ищутся дизъюнкты P в D1 и P в D2. Если таковые найдены, то формируется дизъюнкция этих предложений с исключение P и P. Полученная резольвента добавляется в базу (множество предложений).

18 Технологии ИИ18 Текст программы. Начало 1.% Программа доказательства теорем на основе принципа резолюций 2.domains 3. term = t(integer, symbol); 4. t2(integer, symbol, symbol); 5. t3(integer, symbol, symbol, symbol) tlist = term * % список термов 8.predicates 9. start 10. compare(term, term) 11. end(tlist) 12. resolstep(tlist, tlist, tlist) 13. unify(symbol, symbol) 14. isvar(symbol) 15. isconst(symbol) % Соединение двух списков (деление списка на 2 части) 18. a2(tlist, tlist, tlist) 19. % Выбор очередного элемента из списка 20. eget(tlist, term) % (i,o) 21. % Удаление элемента из списка 22. remove(tlist, term, tlist) % (i,i,o) 23.database 24. sent(tlist) 25.goal 26. % Загружаем предложения 27. retractall(_), 28. consult("resol.db"), 29. start.

19 Технологии ИИ19 Программа. Продолжение 1.clauses 2. % Запуск программы 3. start:- 4. sent(C1), 5. sent(C2), 6. resolstep(C1, C2, C1vC2), 7. not(end(C1vC2)), 8. % Добавляем резольвенту 9. asserta(sent(C1vC2)), !, 10. start. 11. % Шаг резолюции. На входе - предложения С1 и С2. Далее 12. % из них выделяются дизъюнкты E1 и E2. Дизъюнкты 13. % сопоставляются и, в случае обнаружения соответствия 14. % вида (~P и P), формируется резольвента CAvCB. Результат заносится в БД. 15. resolstep(C1, C2, CAvCB):- 16. % извлекаем из С1 и C2 элементы E1 и E2 17. eget(C1, E1), eget(C2, E2), 18. write(" E1=",E1, ", E2=",E2,"\n"), 19. % далее сопоставляем подвыражения 20. compare(E1, E2), 21. % удаляем подвыражение E1 из С1 и E2 из С2 22. remove(C1, E1, CA), 23. remove(C2, E2, CB), 24. % склеиваем списки, полученные после удаления из них P и ~P 25. a2(CA, CB, CAvCB), !. 26. % Проверка на P и ~P - поиск резольвенты 27. compare(t(N1,X1), t(N2,X2)) :- N1+N2 = 1, unify(X1, X2). 28. compare(t2(N1,NAME,ARG1), t2(N2,NAME,ARG2)) :- N1+N2 = 1, unify(ARG1, ARG2). 29. compare(t3(N1,NAME,ARG11,ARG12), t3(N2,NAME,ARG21, ARG22)) :- 30. N1+N2 = 1, 31. unify(ARG11, ARG21), 32. unify(ARG12, ARG22). 33. % Если список пуст, значит есть противоречие 34. end([]):- write("\n\nОбнаружено противоречие. Теорема доказана.\n"), exit(0). 35. % Проверка на унифицируемость 36. unify(A, A) :- !. 37. unify(A, B) :- isvar(A), isvar(B), !. 38. unify(A, B) :- isvar(A), isconst(B), !. 39. unify(A, B) :- isconst(A), isvar(B), ! isvar(S) :- frontchar(S,Ch,_), Ch>='A', Ch='a', Ch ='A', Ch='a', Ch">

20 Технологии ИИ20 Программа. Окончание 1.% Вспомогательные предикаты 2.a2([], L, L). 3. a2([Head | L1], L2, [Head | L3]) :- a2(L1, L2, L3). 4.eget([H|T],H). 5.eget([_|T],R) :- eget(T,R). 6.remove(L, El, Res) :- 7. a2(L1,[El|L2],L), 8. a2(L1,L2,Res).

21 Технологии ИИ21 Пример с Сидоровым Исходные данные (файл resol.db) : 1.sent([t2(0,"lucky","U"),t3(1,"win","U","lottery")]). lucky(U) win(U, lottery) 2.sent([t2(0,"lucky","Y"),t3(1,"pass","Y","Z")]). lucky(Y) pass(Y,Z). 3.sent([t2(0,"study","Y"),t3(1,"pass","Y","Z")]). study(Y) pass(Y,Z). 4.sent([t2(0,"study","sidorov")]). study(сидоров) 5.sent([t3(0,"pass","X",physics"),t3(0,"win","X","lottery"),t2(1,"happy","X")]). -- pass(X, physics) win(X,lottery) happy(X). 6.sent([t2(1,"lucky","sidorov")]). lucky(сидоров). 7.sent([t2(0,"happy","sidorov")]). happy(сидоров)

22 Технологии ИИ22 Алгоритм унификации 1966, Ж.Питра и (независимо от него) Дж.Робинсон на основе работ Эрбрана создают один из основных алгоритмов ИИ – алгоритм унификации. Основной объект - терм. Терм – n-арный объект вместе с n термами. Должны существовать априори исходные термы, являющиеся объектами.

23 Технологии ИИ23 Префиксная форма E преф =log + y - y 2 / b sin x E инф = x 2 +(x+ 3) 2 E инф = y+ 3

24 Технологии ИИ24 Идея алгоритма E инф = cos 2 (a+1)+sin 2 (a+1) T = cos 2 (X)+sin 2 (X)->1

25 Технологии ИИ25 Программа унификации 1.program UnifDemo; 2.procedure replace(var S: string; n: integer; v: string); 3.begin 4. delete(S, n, 1); 5. Insert(v, S, n); 6.end; 7.type 8. TVarN = record 9. Name, Val: string; 10. end; 11.const 12. MaxVar = 100; 13.var 14. VarNum : integer; 15. VarList: array[1..MaxVar] of TVarN; 16.function AddVar(v: char; t: string): boolean; 17.var i:integer; 18.begin 19. AddVar := false; 20. for i:=1 to VarNum do 21. begin 22. if VarList[i].Name = v then 23. if VarList[i].Val = t then AddVar := true; 24. exit; 25. end; 26. VarNum := VarNum+1; 27. if VarNum>MaxVar then error('too many vars'); 28. VarList[VarNum].Name := v; 29. VarList[VarNum].Val := t; 30. AddVar := true; 31.end;

26 Технологии ИИ26 Программа. Продолжение function SUBST(var E1, E2: string; v: char; t: string; h1, h2: integer): boolean; { v - свободная переменная, t - терм, h1 - индекс в выражении E1, h2 - индекс в выражении E2} var i: integer; begin SUBST := false; { Просмотр терма t на предмет поиска недопустимых в нем переменных} for i:=1 to length(t) do if t[i]=v then exit; { Просмотр E1 } i:=h1; while i

27 Технологии ИИ27 Программа. Продолжение 1.function is_operator(c: char): boolean; 2.Begin is_operator := (c in['+','-','*','/','\','~','^','&','|','=']); end; 3.function is_constant(c: char): boolean; 4.Begin is_constant := (c in['a'..'z']) or (c in['0'..'9']); end; 5.function is_var(c: char): boolean; 6.Begin is_var := (c in['A'..'Z']); end; 7.function getterm(E: string; n: integer): string; 8.var 9. t: string; 10. i: integer; 11. cnt: integer; 12. eoj: boolean; 13.begin 14. t := ''; 15. cnt := 1; 16. i := n; 17. eoj := false; 18. while not eoj do 19. begin 20. t := t+E[i]; 21. if is_operator(E[i]) then 22. cnt:=cnt else 24. cnt := cnt-1; 25. i := i+1; 26. eoj:= (i>length(E)) or (cnt=0); 27. end; 28. getterm := t; 29.end;

28 Технологии ИИ28 Программа. Продолжение 1.function Unificate(E1, E2: string) : boolean; 2.{ E1, E2 - унифицируемые выражения } 3.var 4. h1, h2: integer; 5. t: string; 6.begin 7. Unificate := false; 8. h1 := 1; { начальное выражение - символ из E1 } 9. h2 := 1; { начальное_выражение - символ из E2 } 10. { Просмотреть параллельно Expr1 и Expr2 } 11. VarNum := 0; 12. while h2

29 Технологии ИИ29 Программа. Продолжение 1.type 2. TTheoreme = record 3. { T - теорема T=(H,C) } 4. H, C: string; {H(гипотеза) -> C(заключение)} 5. end; 6.const 7. Tnum = 6; 8. TT:array[1..Tnum] of TTheoreme = 9. ((H:'-XX';C:'0'), 10. (H:'+0X';C:'X'), 11. (H:'+X0';C:'X'), 12. (H:'*X1';C:'X'), 13. (H:'*1X';C:'X'), 14. (H:'/X1';C:'X')); 15.var 16. Expr: string; 17. res : boolean; 18. t: string; 19. i, n, k: integer; 20. Cons: string;

30 Технологии ИИ30 Программа. Окончание 1.begin 2. Expr := '+-*ab*ab*1e'; {E=2*a-2*a} 3. i := 1; 4. while i

31 Технологии ИИ31 Пример работы программы Expr: +-*ab*ab*1e ( "-*ab*ab" with "-XX" -> "0") -> +0*1e ( "+0*1e" with "+0X" -> "*1e") -> *1e ( "*1e" with "*1X" -> "e") -> e Result: e "0") -> +0*1e ( "+0*1e" with "+0X" -> "*1e") -> *1e ( "*1e" with "*1X" -> "e") -> e Result: e">

32 Технологии ИИ32 Системы автоматического доказательства теорем Отличие систем автоматического доказательства теорем (или системы автоматизированного формирования рассуждений) от языков логического программирования: обычно поддерживают полную логику первого порядка; синтаксическая форма, выбранная для высказываний, не влияет на результаты; управляющая информация обычно хранится отдельно от БЗ, а не входит в состав самого представления знаний большинство исследований в области САД посвящено поиску стратегий управления, которые приводят к общему повышению эффективности, а не только к увеличению быстродействия.

33 Технологии ИИ33 Система Otter Программа автоматического доказательства теорем Otter (Organized Techniques for Theorem-proving and Effective Research). Подготавливая любую задачу для программы Otter, пользователь должен разделить знания на четыре части: Множество выражений, известное как множество поддержки, в котором определяются важные факты о данной задаче. На каждом этапе резолюции операция резолюции применяется к одному из элементов множества поддержки и к другой аксиоме, поэтому поиск сосредоточивается на множестве поддержки. Множество полезных аксиом (usable axiom), которое выходит за пределы множества поддержки. Эти аксиомы предоставляют фоновые знания о проблемной области. Множество уравнений, известных как правила перезаписи (rewrites), или демодуляторы (demodulators). Демодуляторы представляют собой уравнения. Например: х+0=х (любой терм в форме х+0 должен быть заменен термом х). Множество параметров и выражений, которое определяет стратегию управления. В частности - задание эвристической функции для управления поиском и функцию фильтрации для устранения некоторых подцелей как не представляющих интереса.

34 Технологии ИИ34 Как работает Otter Принцип постоянного применения правила резолюции к одному из элементов множества поддержки и к одной из полезных аксиом. В отличие от системы Prolog, в этой программе используется определенная форма поиска по первому наилучшему совпадению. Ее эвристическая функция измеряет "вес" каждого выражения с учетом того, что наиболее предпочтительными являются выражения с наименьшими весами. Единичные выражения оцениваются как имеющие наименьший вес. На каждом этапе программа Otter перемещает выражение "с наименьшим весом" из множества поддержки в список полезных аксиом и добавляет в множество поддержки некоторые непосредственные следствия применения операции резолюции к выражению с наименьшим весом и к элементам списка полезных аксиом. Программа Otter останавливается, если обнаруживает противоречие или если возникает такая ситуация, что в множестве поддержки не остается больше выражений.

35 Технологии ИИ35 Алгоритм procedure Otter(sos, usable) inputs: sos-- множество поддержки – выражения, определяющие -- решаемую задачу (глобальная переменная) usable-- множество фоновых значений, которые потенциально -- могут быть релевантными для данной задачи repeat clause элемент множества sos с наименьшим весом; переместить выражение clause из множества sos в множество usable; Process(Infer(clause, usable), sos) until sos=[] or function Infer(clause, usable) returns множество выражений clauses применить правило резолюции к выражению clause и каждому элементу множества usable; возвратить полученное множество clauses после применения функции Filter procedure Process(clauses, sos) for each clause in clauses do clause Simplify(clause) выполнить слияние идентичных литералов; отбросить выражение clause, если оно представляет собой тавтологию sos [clause | sos] if clause не имеет литералов, то обнаружено опровержение if clause имеет один литерал, то искать единичное опровержение

36 Технологии ИИ36 Расширение системы Prolog РТТР (Prolog Technology Theorem Prover). 1. В процедуру унификации снова вводится проверка вхождения для того, чтобы эта процедура стала непротиворечивой. 2. Поиск в глубину заменяется поиском с итеративным углублением. Это позволяет добиться того, чтобы стратегия поиска стала полной, а увеличение продолжительности поиска измерялось лишь постоянной зависимостью от времени. 3. Разрешается применение отрицаемых литералов (таких как P(x)). В этой реализации имеется две отдельные процедуры; в одной из них предпринимается попытка доказать Р, а в другой доказать P 4. Выражение с n атомами хранится в виде n различных правил. Например, при наличии в базе знаний выражения A B C должно быть также предусмотрено хранение в ней этого выражения, представленного как B C A и как C B A. 5. Логический вывод сделан полным (даже для нехорновских выражений) путем добавления правила резолюции с линейным входным выражением: если текущая цель унифицируется с отрицанием одной из целей в стеке, то данная цель может рассматриваться как решенная (один из способов рассуждения от противного). Если первоначальной целью было высказывание Ρ и эта цель свелась в результате вывода к цели P, то установлено, что P P. А это выражение логически эквивалентно Р.

37 Технологии ИИ37