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

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

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

Для этих трех формулотсутствуют потенциальноконтрарные формулы(13шагов). Четвертыйпроцессор переходит к п. 4, отменяем последнее действие п. 3.5 (12 шагов),понижаем приоритет отождествления формул V  y3 , y2 , y1  и V  x2 , x5 , x1  до 0 (1шаг).

Выбираем для четвертого процессора новую потенциально контрарнуюформулу V  x4 , x3 , x2  (1 шаг).Для пятого процессора кандидатами на новую рабочую формулу являютсяV  y1 , x2 , x1  , V  y1 , x5 , x1  , V  x1 , y1 , x2  , V  x2 , x1 , y1  и L x2 , y1, x5  , но ни одна изних не имеет потенциально контрарных формул (25 шагов). Пятый процессорпереходит к п. 4, отменяем последнее выполнение п.

3.5 (10 шагов), понижаемприоритет отождествления формул V  y3 , y4 , y2  и V  x2 , x5 , x1  до 0 (1 шаг).Выбираем для пятого процессора новую потенциально контрарную формулуV  x3 , x1, x4  (1 шаг).Итого на эту итерацию потребовалось 48 шагов.Согласно п.

3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого65555процессора l1  1, l2  2, l3  2, l4  1, l5  1 (1 шаг)ПРОЦЕССОРПЕРВЫЙ ВТОРОЙ ТРЕТИЙ ЧЕТВЕРТЫЙ ПЯТЫЙy1  x3y 2  x4y3  x1y1  x2y 2  x3y3  x 4y3  x 4y 4  x3y 2  x4y3  x3y 4  x1134Решения всех процессоров попарно противоречивы (11 шагов).Согласно п. 3.5 имеем следующие пять F-наборовпервый процессор V  x3 , x1, x4   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x3 , y4 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x4 , x3 , x1   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x1, x4 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x1, y4 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3Lx,x,yLx,x,x1 3 44 2 5на замену всех вхождений переменных на их значения уходит 12 шагов;второй процессор  V  x1, x4 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 V  x1, x2 , x3   V  x1, x2 , x3   V  x2 , x5 , x1     V  x , x , x   V  x , x , x   V  x , x , x  3 1 44 3 24 5 3 Vx,x,xVx,x,xVx,x,xVx,x,x3 1 41 2 32 4 12 5 1 V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x4 , x3 , x1   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3  V  x4 , x2 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 L x4 , x1, x2   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага;третий процессор135  V  x4 , x1, x2   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x4 , x3 , x2   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 V  x2 , x4 , x1   V  x2 , x4 , x1     V  x , x , x   V  x , x , x   V  x , x , x  3 1 44 3 24 5 3   V  x1, x2 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3  V  x1, x3 , x2   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 L x1, x4 , x3   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 2 шага;четвертый процессор  V  x2 , x4 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x , y , x    V  x , x , x   V  x , x , x    V  x , x , x   2 4 31 2 32 4 12 5 1  V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x3 , x2 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 V  x4 , x3 , x2   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x , y , x    V  x , x , x   V  x , x , x    V  x , x , x    4 4 31 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Lx4 , x2 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;пятый процессор136 V  y1, x3 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1       V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  y1, x1, x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1       V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x4 , y1, x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3 V  x3 , x4 , y1   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      Vx,x,xVx,x,xVx,x,x314432453V  x3 , x1, x4   V  x3 , x1, x4   V  x4 , x5 , x3 Lx3 , y1, x1   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 10 шагов.Таким образом, на выполнение п.

3.5 потрачено 12 шагов.Пустой F-набор не выведен (6 шагов), но первый, второй, третий ичетвертый процессоры вывели тупиковые F-наборы (6 шагов). Для всех этихпроцессоров не найдены новые тавтологичные формулы (12 шагов у первого ичетвертого процессоров, 19 шагов у второго и третьего процессоров). Ищемновые рабочие формулы для всех процессоров.Для первого процессора кандидатами на новую рабочую формулу являютсяV x3 , y4 , x4  ,V  x1 , y4 , x4  и L x1, x3 , y4  (3 шага). Для этих трех формулотсутствуют потенциально контрарные формулы (13 шагов). Первый процессорпереходит к п. 4, отменяем последнее действие п.

3.5 (12 шагов), понижаемприоритет отождествления формул V  y1, y3 , y2  и V  x3 , x1, x4  до 0 (1 шаг).Выбираем для первого процессора новую потенциально контрарную формулуV  x4 , x3 , x2  (1 шаг).У второго процессора присвоены значения всем переменным (6 шагов).Переходим к п. 4, отменяем последнее применения п. 3.5 (4 шага). Для формулV  x1 , y3 , x3  , V  x3 , x1 , y3  , V  y3 , x3 , x1  , V  y3 , x2 , x3  и L y3 , x1, x2  нет новыхподходящих для отождествления (25 шагов). Переходим к п. 4, отменяемпоследнее применение п. 3.5 (10 шагов), понижаем приоритет отождествления137формул V  y1, y4 , y2  и V  x1 , x2 , x3  до 0 (1 шаг). Выбираем для второгопроцессора новую потенциально контрарную формулу V  x2 , x5 , x1  (1 шаг).У третьего процессора присвоены значения всем переменным (6 шагов).Переходим к п.

4, отменяем последнее применения п. 3.5 (2 шага). Для формулV x4 , y4 , x2  ,V  x1 , y4 , x2 иL x1, x4 , y4 нетновыхподходящихдляотождествления (13 шагов). Переходим к п. 4, отменяем последнее применение п.3.5 (12 шагов), понижаем приоритет отождествления формул V  y2 , y1, y3  иV  x2 , x4 , x1  до 0 (1 шаг). Выбираем для третьего процессора новуюпотенциально контрарную формулу V  x3 , x1, x4  (1 шаг).Для четвертого процессора выбираем новую рабочую формулу V  x4 , y4 , x3 (8 шагов). Для этой формулы потенциально контрарной формулой являетсяV  x4 , x5 , x3  (5 шагов).Для пятого процессора новой рабочей формулой являются V  x4 , y1, x3  (3шага). Выбираем для первого процессора новую потенциально контрарнуюформулу V  x4 , x5 , x3  (6 шагов).Итого на эту итерацию потребовалось 72 шага.Согласно п.

3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого76666процессора l1  1, l2  1, l3  1, l4  2, l5  1 (1 шаг)ПРОЦЕССОРПЕРВЫЙВТОРОЙТРЕТИЙy1  x4y 2  x2y3  x3y1  x2y 2  x1y1  x1y 2  x3y3  x 4y 4  x5ЧЕТВЕРТЫЙПЯТЫЙy1  x5y 4  x5Решения всех процессоров попарно противоречивы (11 шагов).138Согласно п. 3.5 имеем следующие шесть F-наборовпервый процессор V  x4 , x3 , x2   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x , y , x   V  x , x , x   V  x , x , x   V  x , x , x   4 4 21 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x2 , x4 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x3 , x2 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x3 , y4 , x2   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Lx3 , x4 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;второй процессор V  x2 , y3 , x1   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1       V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Vx,x,xVx,x,x251251  V  x , x , x   V  x , x , x   V  x , x , x  3 1 44 3 24 5 3   V  x , x , y   V  x , x , x    V  x , x , x    V  x , x , x    1 2 31 2 32 4 12 5 1  V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  y , x , x   V  x , x , x    V  x , x , x    V  x , x , x    3 1 21 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  y , x , x   V  x , x , x   V  x , x , x   V  x , x , x    3 5 11 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 L y3 , x2 , x5   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 10 шагов;третий процессор139  V  x1 , x4 , x3   V  x1 , x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1 , x4   V  x4 , x3 , x2   V  x4 , x3 , x5  V  x , y , x   V  x , x , x    V  x , x , x    V  x , x , x   1 4 31 2 32 4 12 5 1  V  x3 , x1 , x4   V  x4 , x3 , x2   V  x4 , x3 , x5  V  x3 , x1 , x4   V  x3 , x1 , x4   V  x4 , x3 , x2   V  x4 , x3 , x5    V  x , x , x   V  x , x , x   V  x , x , x   V  x , x , x    4 3 11 2 32 4 12 5 1Vx,x,xVx,x,xVx,x,x3 1 44 3 24 3 5  V  x , y , x   V  x , x , x    V  x , x , x    V  x , x , x    4 4 31 2 32 4 12 5 1   V  x3 , x1 , x4   V  x4 , x3 , x2   V  x4 , x3 , x5 Lx4 , x1 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;четвертый процессор  V  x2 , x4 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x2 , x5 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x3 , x2 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 V  x4 , x3 , x2   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x4 , x5 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 L x4 , x2 , x5   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 2 шага;пятый процессор140  V  x5 , x3 , x4   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Vx,x,xVx,x,xVx,x,xVx,x,x5 1 41 2 32 4 12 5 1 V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x4 , x5 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x3 , x4 , x5   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 V  x3 , x1, x4   V  x3 , x1, x4   V  x4 , x5 , x3 Lx,x,xLx,x,x3 5 14 2 5на замену всех вхождений переменных на их значения уходит 10 шагов.Таким образом, на выполнение п.

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

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