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

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

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

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

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

Выбираем для первого процессора новую потенциальноконтрарную формулуV  x4 , x3 , x5  (1 шаг).141Для второго процессора новой рабочей формулой являются V  x2 , y3 , x1  (1шаг), выбираем потенциально контрарную ей V  x2 , x4 , x1  (2 шага).У третьего процессора новой рабочей формулой является V  x1, y4 , x3  (1шага). Выбираем для неѐ подходящую для отождествления формулу V  x1 , x2 , x3 (1 шаг).У четвертого процессора присвоены значения всем переменным (6 шагов).Переходим к п.

4, отменяем последнее применения п. 3.5 (4 шага). Для формулV  x2 , y4 , x3  ,V  x4 , y4 , x3 L  x4 , x2 , y 4 инетновыхподходящихдляотождествления (13 шагов). Переходим к п. 4, отменяем последнее применение п.3.5 (12 шагов), понижаем приоритет отождествления формул V  y3 , y2 , y1  иV  x4 , x3 , x2  до 0 (1 шаг).

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

3.5 (10 шагов), понижаем приоритет отождествления формулV  y3 , y4 , y2  и V  x3 , x1, x4  (1 шаг), выбираем новую потенциально контрарнуюформулу V  x4 , x5 , x3  (1 шаг).Итого на эту итерацию потребовалось 62 шага.Согласно п. 3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого87787процессора l1  1, l2  2, l3  2, l4  1, l5  1 (1 шаг)ПРОЦЕССОР142ПЕРВЫЙy1  x4y2  x5y3  x3ВТОРОЙТРЕТИЙЧЕТВЕРТЫЙПЯТЫЙy1  x5y2  x3y3  x4y2  x3y3  x4y 4  x2y3  x4y4  x5Решения всех процессоров попарно противоречивы (11 шагов).Согласно п.

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

3.5 потрачено 12 шагов.Пустой F-набор не выведен (6 шагов), но первый, второй, третий ичетвертый процессоры вывели тупиковые F-наборы (6 шагов). Для второгопроцессора найдена новая тавтологичная формула Lx4 , x2 , x5   Lx4 , x2 , x5 (24 шага), увеличиваем длину фрагмента для этого процессора l28  3 , теперьфрагмент имеет вид L x4 , x2 , x5  & V  x2 , x4 , x1  & V  x2 , x5 , x1  .

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

У первого процессора больше нет новых потенциальноконтрарных формул (1 шаг), процессор заканчивает работу.У второго процессора присвоены значения всем переменным (6 шагов).Переходим к п. 4, отменяем последнее применения п. 3.5 (4 шага). Новой рабочей145формулой является V  x1, x2 , y3  (2 шага). Выбираем для второго процессорановую потенциально контрарную формулу V  x1, x2 , x3  (1 шаг).У третьего процессора присвоены значения всем переменным (6 шагов). Онпереходит к п. 4, отменяем последнее действие п. 3.5 (10 шагов), понижаемприоритет отождествления формул V  x1, y4 , x3  и V  x1, x2 , x3  до 0 (1 шаг). Длятретьего процессора кандидатами на новую рабочую формулу являютсяV  x1, y4 , x3  ,V  x4 , y4 , x3  и L x4 , x1, y4  формулы (3 шага), но для них нет новыхпотенциально контрарных (13 шагов), отменяем последнее действие п.

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

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

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