Технологии ИИ1 ТЕХНОЛОГИИ ИСКУССТВЕННОГО ИНТЕЛЛЕКТА Лекция 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 Определения Определение. Формальное доказательство – это конечная последовательность формул M 1, M 2, …, M r таких, что каждое M i – либо аксиома, либо M i выводима при помощи одного из правил вывода из предшествующих формул M j, j

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

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

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

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

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

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

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

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

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

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

Технологии ИИ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 Текст программы. Начало 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 Программа. Продолжение 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

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

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

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

Технологии ИИ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 Программа. Продолжение 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 Программа. Продолжение 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 Программа. Продолжение 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 Программа. Продолжение 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 Программа. Окончание 1.begin 2. Expr := '+-*ab*ab*1e'; {E=2*a-2*a} 3. i := 1; 4. while i

Технологии ИИ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

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

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

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

Технологии ИИ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 Расширение системы 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