Диссертация (1150569), страница 15

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 15)

1 будет следующий F-набор:  V  x2 , x1, x4   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )   V(a,a,a)V(a,a,a)V(a,a,a)V(a,a,a)3 4 54 2 34 3 65 3 6V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x4 , x2 , x3   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V ( a , a , a )  V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   3 4 54 2 34 3 65 3 6V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x , x , x   V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   4 3 61 2 32 1 43 1 4V(a,a,a)V(a,a,a)V(a,a,a)V(a,a,a)D : 3 4 54 2 34 3 65 3 6V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x6 , x4 , x5   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V ( a , a , a )  V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   3 4 54 2 34 3 65 3 6 V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )Lx,x,xV(a,a,a)V(a,a,a)V(a,a,a)426123214314  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 692На выполнение п.

1 алгоритма IMA потребовалось 5 шагов.П. 2.1 на этом этапе не применяется. Согласно п. 2.2, берем формулуV  x2 , x1, x4  , согласно п. 2.3 берем отрицание атомарной формулы с тем жепредикатным символом V (a1, a2 , a3) (2 шага), и помечаем его как уделенное (5шагов). Согласно п. 2.4 решаем систему уравнений, отождествляющую эти двеформулы:x2  a1x1  a2x4  a3(3 шага)Согласно п. 2.5 рассматриваемый F-набор D приобрел вид  V a1, a2 , a3   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , a , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   3 1 31 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , x , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   3 3 61 2 32 1 43 1 4V(a,a,a)V(a,a,a)V(a,a,a)V(a,a,a)D:3 4 54 2 34 3 65 3 6  V(a,a,a)L(a,a,a)L(a,a,a)645315426  V  x , a , x   V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   6 3 51 2 32 1 43 1 4V(a,a,a)V(a,a,a)V(a,a,a)V(a,a,a)3 4 54 2 34 3 65 3 6  V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  La3 , a1, x6   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )    V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 693на замену всех вхождений переменных на их значения уходит 13 шагов.

8На выполнение пп. 2.6 и 2.7 (проверку не получился ли пустой илитупиковый F-набор) затрачено 10 шагов. На выполнение п. 2.8 ушло 5 шагов.Согласно п. 2.9 (4 шага) возвращаемся к п. 2.2 и 2.3. Берем формулу V a3 , a1, x3  иотрицание атомарной формулы с тем же предикатным символом V (a3 , a1, a4 ) (7шагов). Согласно п. 2.4 решаем систему уравнений, отождествляющую эти двеформулыx3  a4(1 шаг)Согласно п.

2.5 рассматриваемый F-набор D приобрел вид  V a1, a2 , a3   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , a , a   V (a , a , a )  V (a , a , a )  V (a , a , a )   3 1 41 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V(a,a,a)L(a,a,a)L(a,a,a)645315426  V a , a , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   3 4 61 2 32 1 43 1 4D :  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x , a , x   V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   6 3 51 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V(a,a,a)L(a,a,a)L(a,a,a)645315426  La3 , a1, x6   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )    V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 6на замену всех вхождений переменных на их значения уходит 6 шагов.89 шагов на подстановку полученных в результате решения системы уравнений значений переменных в Fнаборе и 4 шага на п.

2.6, то есть на проверку наличия повторений формул в F-наборе и их удаление.94На п. 2.6 уходит 5 шагов. Согласно п. 2.7 получился тупиковый F-набор (10шагов), переходим к п. 3 и отменяем последнее действие п. 2.5. РассматриваемыйF-набор D принимает вид  V a1, a2 , a3   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , a , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   3 1 31 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , x , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   3 3 61 2 32 1 43 1 4V(a,a,a)V(a,a,a)V(a,a,a)V(a,a,a)D:3 4 54 2 34 3 65 3 6  V(a,a,a)L(a,a,a)L(a,a,a)645315426  V  x , a , x   V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   6 3 51 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )La,a,xV(a,a,a)V(a,a,a)V(a,a,a)3 1 61 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )    V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 6на обратную замену всех вхождений значений переменных на их имена уходит 2шага.Возвращаемся к 2.3.

У формулы V a3 , a1, x3  нет подходящей дляунификации (8 шагов). Согласно п. 3 рассматриваемы F-набор принимаетисходный вид, но формулы V ( a1, a2 , a3 ) и V (a3 , a1, a4 ) помечены как удаленныеи не принимают участия в переборе (9 шагов).95  V  x2 , x1, x4   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x , x , x    V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   4 2 31 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V(a,a,a)L(a,a,a)L(a,a,a)645315426  V  x , x , x   V ( a , a , a )  V ( a , a , a )   V ( a , a , a )   4 3 61 2 32 1 43 1 4D :   V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x , x , x    V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   6 4 51 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V(a,a,a)L(a,a,a)L(a,a,a)645315426Lx,x,xV(a,a,a)V(a,a,a)V(a,a,a)4 2 61 2 32 1 43 1 4  V ( a , a , a )  V ( a , a , a )  V ( a , a , a )  V ( a , a , a )   3 4 54 2 34 3 65 3 6 V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 6Согласно пп.

2.2 и 2.3 берем формулу V  x2 , x1, x4  и отрицаниеV a2 , a1, a4  (7 шагов). Согласно п. 2.4 решаем систему уравнений,отождествляющую эти две формулыx2  a2x1  a1x4  a4(3 шага)Согласно п. 2.5 рассматриваемый F-набор D приобрел вид96  V a2 , a1, a4   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , a , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   4 2 31 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a , x , x   V (a , a , a )  V (a , a , a )  V (a , a , a )   4 3 61 2 32 1 43 1 4D :   V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x , a , x   V ( a , a , a )  V ( a , a , a )   V ( a , a , a )   6 4 51 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )     V(a,a,a)L(a,a,a)L(a,a,a)645315426La,a,xV(a,a,a)V(a,a,a)V(a,a,a)4 2 61 2 32 1 43 1 4  V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )    V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 6на замену всех вхождений переменных на их значения уходит 13 шагов.Согласно п.

2.9 (5 шагов) возвращаемся к п. 2.2 и 2.3. Берем формулуV a4 , a2 , x3  и отрицание V (a4 , a2 , a3 ) (7 шагов). Согласно п. 2.4 решаемсистему уравнений, отождествляющую эти две формулыx3  a 3(1 шаг)Согласно п. 2.5 рассматриваемый F-набор D приобрел вид97  V a2 , a1, a4   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )   V(a,a,a)L(a,a,a)L(a,a,a)6 4 53 1 54 2 6  V a4 , a2 , a3   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )      V ( a , a , a )   V ( a , a , a )  V ( a , a , a )   V ( a , a , a )   3 4 54 2 34 3 65 3 6V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V a4 , a3 , x6   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )   D :   V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )    V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  V  x6 , a4 , x5   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )     V (a3 , a4 , a5 )  V (a4 , a2 , a3 )  V (a4 , a3 , a6 )  V (a5 , a3 , a6 )    V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )  La4 , a2 , x6   V (a1, a2 , a3 )  V (a2 , a1, a4 )  V (a3 , a1, a4 )      V ( a , a , a )   V ( a , a , a )  V ( a , a , a )   V ( a , a , a )   3 4 54 2 34 3 65 3 6V (a6 , a4 , a5 )  L(a3 , a1, a5 )  L(a4 , a2 , a6 )на замену всех вхождений переменных на их значения уходит 5 шагов.На выполнение пп.

Характеристики

Список файлов диссертации