АЛГОРИТМЫ ПРОВЕРКИ выводимости формул в ИВ: 1) алг-м Квайна; 2) метод редукции; 3) метод резолюций.
1) АЛГОРИТМ КВАЙНА - для проверки тождественной истинности формулы a(X1, ..., Xn) используется семантическое дерево, представляющее собой бинарное однокоренное дерево. Алгоритм квайна позволяет проследить лишь часть дерева и заключается в последовательном переборе переменной Xi и принимаемым им занчений 0 и 1. для кадого такого набора анализируется таблица истинности а(Х1, ..., Хn). Причем эта таблица из-за фмксир. знач. Xi содержит меньшее число переменных.
2) АЛГОРИТМ МЕТОДА РЕДУКЦИИ - при переборе наборов значений переменных исследуемой формулы исп-ся св-во импликации (1(посылка)->0(следствие)=0). пример: (X->Z)->((Y->Z)->(X\/Y->Z))=0. преоложим, что формула тожд. ложна т.е. [X->Z=0, (((Y->Z)->(X\/Y->Z))=0)], упрощаем: [X->Z=0, X\/Y->Z=0)], т.к. следствие должно быть по нашему допушению ложным, то в этом следствии посылка 1, а следствие 0: [X\/Y=1, Z=0] - Z=0 подставляем: X->0=1, Y->0=1; следовательно X=Y=0.
3) МЕТОД РЕЗОЛЮЦИИ - элементарная дизъюнкция - дизъюнкт (Xv(not X)vYvZ). пусть D1=D1'vA; D2=D2'v(not A). D1'vD2' - РЕЗОЛЬВЕНТА дизъюнктов D1 и D2 по переменной A. Резольвентой дизъюнктов D1 и D2 наз-ся резольвента по некторой переменной: res(D1,D2), res[A](D1,D2) [A] - нижний индекс при res, res(A,(not A))=0 т.к. A&(not A)=0. Если дизъюнкты D1 и D2 не содержат противоположных переменных, то res(D1,D2) не существует.
пример: D1=AvBvC; D2=(not A)v(not B)vD. [] - в скобках индексы: res[A](D1,D2)=BvCv(not B)vD; res[B](D1,D2)=AvCv(not A)vD.
ТЕОРЕМА: 1) если res(D1,D2) существует и не равен 0, то D1,D2|-res(D1,D2). 2) если res(D1,D2)=0 => D1,D2 противоречивы.
S=[D1,D2,...Dn] - множество дизъюнктов. ТЕОРЕМА о полноте метода резолюции: мн-во дизъюнктов противоречиво тогда и только тогда, когда существует резольвента вывод. из S, заканчивающийся нулем.
пример: A->(B->C), C^D->E, (not F)->D^(not E)|-A->(B->F). записываем S: S=(A->(B->C), C^D->E, (not F)->D^(not E), (not A->(B->F)) - последнее целиком отрицаем) упрощаем все: A->(B->C)=(not A)v(not B)vС; C^D->E=(not C)v(not D)vE; (not F)->D^(not E)=FvD^(not E)=(FvD)^(Fv(not E)); (not A->(B->F))=A^B^(not F); теперь записывает S с учетом упрощений: S*=[(not A)v(not B)vС, (not C)v(not D)vE, FvD, Fv(not E), A, B, (not F)], т.е. все ^ меняем на ,. затем находим резольвенты из S* - надо брать 2 элемента в которых есть противоположные буквы: 1)res[A]((not A)v(not B)vС; A)=(not B)vC; 2)res[B]((not B)vC; B)=C; 3)res[D]((not C)v(not D)vE; FvD)=(not C)vEvF; 4)res[E]((not C)vEvF; Fv(not E))=(not C)vF; 5)res[C]((not C)vF; C)=F; 6)res[F]((not F); F)=0.
