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

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

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

3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого988процессора l2  2, l3  1, l5  2 (1 шаг)ПРОЦЕССОРВТОРОЙТРЕТИЙПЯТЫЙ146y3  x3y1  x2y 2  x4y3  x3y1  x1Решения всех процессоров попарно противоречивы (3 шага).Согласно п. 3.5 имеем следующие три F-наборавторой процессор  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  x2 , x5 , 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  x1, 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   V  x3 , 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  x3 , 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 x3 , x2 , x5   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага;третий процессор  V  x2 , 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  x , y , x   V  x , x , x    V  x , x , x    V  x , x , x   2 4 41 2 32 4 12 5 1   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 , x , 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  x , y , x   V  x , x , x    V  x , x , x   V  x , x , x    3 4 41 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Lx,x,yLx,x,x3 2 44 2 5на замену всех вхождений переменных на их значения уходит 12 шагов;147пятый процессор  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 Vx,x,xVx,x,xVx,x,xVx,x,x1 5 31 2 32 4 12 5 1 V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   V  x3 , 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 , 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  x4 , x5 , x3   V  x4 , x5 , x3 Lx,x,xLx,x,x4 1 54 2 5на замену всех вхождений переменных на их значения уходит 4 шага.Таким образом, на выполнение п.

3.5 потрачено 12 шагов.Пустой F-набор не выведен (6 шагов), но второй, третий и пятыйпроцессоры вывели тупиковые F-наборы (6 шагов). Для всех процессоров ненайдены новые тавтологичные формулы (25 шагов у второго и пятогопроцессоров и 12 шагов у третьего процессора). Ищем новые рабочие формулыдля всех процессоров.У второго процессора присвоены значения всем переменным (6 шагов). Переходим к п. 4,отменяем последнее применения п. 3.5 (4 шага).

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

3.5 (4 шага). Для пятогопроцессора новой рабочей формулой является V  x4 , x3 , y1  (1 шаг), а новойпотенциально контрарной формулой является V  x4 , x3 , x2  (5 шагов).Итого на эту итерацию потребовалось 72 шага.Согласно п. 3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого10процессора l2 1, l39  2, l59  2 (1 шаг)ПРОЦЕССОРВТОРОЙТРЕТИЙПЯТЫЙy1  x2y1  x3y2  x4y4  x1y4  x1Решения всех процессоров попарно противоречивы (3 шага).Согласно п. 3.5 имеем следующие три F-наборавторой процессор V  x3 , y3 , 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  x , x , x   V  x , x , x   V  x , x , x   V  x , x , x  3 1 43 1 44 3 24 5 3Vx,x,yVx,x,xVx,x,xVx,x,x4 3 31 2 32 4 12 5 1  Vx,x,xVx,x,xVx,x,x314432453Vy,x,xVx,x,xVx,x,xVx,x,x3 4 31 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3  V  y3 , 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 L y3 , x3 , x1  L x4 , x2 , x5на замену всех вхождений переменных на их значения уходит 10 шагов;третий процессор149  V  x2 , 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2 1 41 2 32 4 12 5 1 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  x3 , x4 , 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  x3 , 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 L x3 , x2 , x1   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  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  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 , x5 , x3   V  x4 , x5 , x3 Lx,x,xLx,x,x4 2 54 2 5на замену всех вхождений переменных на их значения уходит 4 шага.Таким образом, на выполнение п.

3.5 потрачено 10 шагов.Пустой F-набор не выведен (6 шагов), но второй, третий и пятыйпроцессоры вывели тупиковые F-наборы (6 шагов). Для пятого процессоранайдена новая тавтологичная формула Lx4 , x2 , x5   Lx4 , x2 , x5  (25 шагов),увеличиваем длину фрагмента этого процессора на 1 l510  3 (1 шаг), запоминаемсоответствующий фрагмент V  x4 , x3 , x2  & V  x4 , x5 , x3  & L x4 , x2 , x5  (1 шаг). Для150остальных процессоров не найдены новые тавтологичные формулы (25 шагов увторого процессора и 12 шагов у третьего).

Ищем новые рабочие формулы длявсех процессоров.У второго процессора новой рабочей формулой являетсяV x4 , x3 , y3 для второго процессора новую потенциально контрарную формулу(8 шагов), ВыбираемV  x4 , x3 , x2  (5шагов).У третьего процессора присвоены значения всем переменным (6 шагов).Переходим к п. 4, отменяем последнее применения п. 3.5 (2 шага). Кандидатамина новую рабочую формулу являются V  x2 , y4 , x4  ,V  x3 , y4 , x4  и L x3 , x2 , y4  (3шага), но ни одна из них не имеет новой потенциально контрарной формулы (13шагов). Переходим к п. 4, отменяем последнее применения п.

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

3.5 (4 шага). Для пятогопроцессора нет новой рабочей формулы (1 шаг), переходим к п. 4, отменяемпоследнее применения п. 3.5 (1 шаг). У пятого процессора больше нет новыхпотенциально контрарных формул (1 шаг), процессор заканчивает работу.Итого на эту итерацию потребовалось 56 шагов.Согласно п. 3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого1110процессора l2  2, l3 1 (1 шаг)ПРОЦЕССОРВТОРОЙТРЕТИЙ151y3  x 2y1  x3y 2  x4y3  x5Решения процессоров противоречивы (1 шаг).Согласно п. 3.5 имеем следующие два F-наборавторой процессор  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 , x1, x4   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3    V  x , x , x   V  x , x , x    V  x , x , x   V  x , x , x    4 3 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  x2 , 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 L x2 , x3 , x1   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага;третий процессор  V  x3 , x5 , 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  x , y , x    V  x , x , x   V  x , x , x    V  x , x , x   3 4 41 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 V  x4 , x5 , x3   V  x4 , x5 , x3   V  x , x , x    V  x , x , x   V  x , x , x    V  x , x , x    5 4 31 2 32 4 12 5 1  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    5 4 41 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Lx,x,yLx,x,x5 3 44 2 5на замену всех вхождений переменных на их значения уходит 12 шагов.152Таким образом, на выполнение п.

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

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