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

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

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

3.5 равно наибольшему из этих шестичисел, то есть 12 шагов.Пустой F-набор не выведен (6 шагов), но первый, третий и четвертыйпроцессоры вывели тупиковые F-наборы (6 шагов), новых тавтологичных формулне найдено ни для одного процессора (17 шагов у каждого процессора). Ищемновые рабочие формулы для этих процессоров.118Для первого процессора это сначала V  x1 , y4 , x3  (1 шаг), но для неѐотсутствует подходящая потенциально контрарная формула (6 шагов), потомV  x2 , y4 , x3  (1 шаг), затем L x2 , x1 , y4  (1 шаг), но и для них отсутствуютпотенциально контрарные формулы (7 шагов). Таким образом, первый процессорпереходит к п. 4.

Отменяем для него последнее действие п.3.5 (12 шагов), теперьдлина фрагмента равнаl1  0(1 шаг), присваиваем нулевой приоритетприсвоению, выполненному в п. 3.3 (1 шаг). Берем для первого процессора новуюпотенциально контрарную формулу V  x2 , x4 , x1  (1 шаг).Берем для второго процессора новую рабочую формулу V  x2 , y3 , x1  иследующую потенциально контрарную формулу V  x2 , x5 , x1  (4 шага). Длявторого процессора увеличивается процессоров длина фрагментаитеперьфрагментвторогопроцессоравыглядит(1 шаг)l2  2следующимобразомV  x2 , x4 , x1  & V  x2 , x5 , x1  .Для третьего процессора это V  x5 , y4 , x2  , V  x1 , y4 , x2  и L y3 , x2 , x4  (3 шагана перебор трех формул).

Для всех трех формул отсутствуют потенциальноконтрарные (13 шагов). Теперь третий процессор переходит к п. 4. Отменяем длянего последнее действие п.3.5 (12 шагов), теперь длина фрагмента равнаl3  0(1 шаг), присваиваем нулевой приоритет присвоению, выполненному в п. 3.3 (1шаг). Берем для третьего процессора новую потенциально контрарную формулуV  x1, x2 , x3  (1 шаг).Для четвертого процессора это V  x4 , y4 , x1  , V  x3 , y4 , x1  и L y3 , x2 , x4  (3шага). Для этих трех формул тоже отсутствуют потенциально контрарные (13шагов).

Теперь четвертый процессор переходит к п. 4. Отменяем для негопоследнее действие п.3.5 (12 шагов), длина фрагмента равна l4  0 (1 шаг),присваиваем нулевой приоритет присвоению, выполненному в п. 3.3 (1 шаг).119Берем для четвертого процессора новую потенциально контрарную формулуV  x1, x2 , x3  (1 шаг).Берем для пятого процессора новую рабочую формулу V  y1 , x4 , x2  , но онане имеет потенциально контрарной (7 шагов), теперь берем V  y1 , x3 , x2  (1 шаг),но и она не имеет потенциально контрарной (6 шагов).

Так же, как и V  x2 , y1 , x4  ,V  x4 , x2 , y1  и L y3 , x2 , x4  (13 шагов). Отменяем для пятого процессора последнеедействие п. 3.5 (10 шагов), уменьшаем приоритет отождествления списков y3 , y4 , y2  и x4 , x3 , x2  (1 шаг)контрарную формулу V  x1 , x2 , x3  (1 шаг).переменныхи берем новую потенциальноИщем шестого процессора новую рабочую формулу V  x2 , x4 , y2  иследующуюпотенциальноконтрарнуюформулуV  x2 , x4 , x1  (3 шага).Увеличивается для шестого процессора длину фрагмента l6  2 (1 шаг) и теперьфрагментшестогопроцессоравыглядитследующимобразомV  x2 , x4 , x1  & V  x2 , x5 , x1  .Всего на эту итерацию требуется наибольшее количество шагов,затраченное каким-либо процессором.

В нашем случае это 54 шага у первого(третьего или четвертого) процессора.Согласно п. 3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого222222процессора l1  1, l2  2 , l3  1, l4  1, l5  1, l6  2 (1 шаг)ПРОЦЕССОРПЕРВЫЙy1  x2y2  x1y3  x4ВТОРОЙТРЕТИЙЧЕТВЕРТЫЙПЯТЫЙШЕСТОЙy1  x3y 2  x2y3  x1y2  x3y2  x1y3  x5y1  x2y2  x1y3  x3y3  x1y4  x2120Решения всех процессоров попарно противоречивы (16 шагов).Согласно п.

3.5 имеем следующие шесть F-наборовпервый процессор V  x2 , x4 , x1   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x , x , x   V  x , x , x   V  x , x , x  3 1 44 3 24 5 3  V  x , y , x   V  x , x , x   V  x , x , x   V  x , x , x   2 4 11 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x1, 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 , 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 , y4 , 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 L x4 , x2 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит12 шагов;второй процессор  V  x2 , x5 , 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Vx,x,xVx,x,x2 4 11 2 32 4 12 5 1 V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x1, x2 , 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  x5 , x1, x2   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  x5 , x4 , x1   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3L x5 , x2 , x4   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага;третий процессор121  V  x2 , 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  x , y , x   V  x , x , x   V  x , x , x   V  x , x , x   2 4 11 2 32 4 12 5 1  V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  x1, x2 , x3   V  x1, x2 , x3   V  x2 , x4 , x1     V  x , x , x   V  x , x , x   V  x , x , x  3 1 44 3 24 5 3   V  x3 , 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 Vx,y,xVx,x,xVx,x,xVx,x,x3 4 11 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Lx3 , x2 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;четвертый процессор  V  x3 , 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  x , y , x   V  x , x , x   V  x , x , x   V  x , x , x   3 4 21 2 32 4 12 5 1  V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x2 , 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, x2 , x3   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     V  x4 , x3 , x2   V  x4 , x5 , x3  V  x1, 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x1, x3 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;пятый процессор122 V  y1 , x1 , 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  y1 , x2 , 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  x3 , y1 , x1   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  x1 , x3 , y1   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 3 5  V  x , x , x   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 , x5 Lx1 , y1 , x2   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 10 шагов;шестой процессор  V  x2 , x4 , 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  x2 , x5 , 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, 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 , x1, x2   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 , x5 , x1   V  x1, x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1     Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3L x4 , x2 , x5   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага.Таким образом, на выполнение п.

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

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