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

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

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

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

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

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

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

4, отменяемпоследнее действие п. 3.5 (10 шагов), понижаем приоритет отождествленияформул L y3 , y1 , y 4  и L x4 , x2 , x5  до 0 (1 шаг). Для шестого процессора нет ниодной потенциально контрарной формулы (1 шаг), процессор заканчивает работу.Итого на эту итерацию потребовалось 72 шага.Согласно п.

3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого54444процессора l1  1, l2  1, l3  1, l4  1, l5  1 (1 шаг)ПРОЦЕССОРПЕРВЫЙ ВТОРОЙ ТРЕТИЙ ЧЕТВЕРТЫЙ ПЯТЫЙy1  x2y 2  x1y 3  x5y1  x1y 2  x3y1  x4y 2  x2y3  x1y1  x1y 2  x5y3  x 2y 4  x2y 2  x1y3  x 2y 4  x5Решения всех процессоров попарно противоречивы (11 шагов).Согласно п. 3.5 имеем следующие пять F-наборовпервый процессор130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  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 , 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     V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Vx,y,xVx,x,xVx,x,xVx,x,x5 4 11 2 32 4 12 5 1   V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Lx5 , x2 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;второй процессор V  x1, y3 , 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   V  x , x , y   V  x , x , x    V  x , x , x   V  x , x , x    3 1 31 2 32 4 12 5 1 Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3  V  y , x , x   V  x , x , x    V  x , x , x   V  x , x , x    3 3 11 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 2 31 2 32 4 12 5 1  Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3Ly,x,xLx,x,x3 1 24 2 5на замену всех вхождений переменных на их значения уходит 10 шагов;третий процессор131  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  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 , 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     V  x3 , x1, x4   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, x4 , y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;четвертый процессор  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  x , y , x   V  x , x , x   V  x , x , x   V  x , x , x   1 4 51 2 32 4 12 5 1   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      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3 Vx,x,xVx,x,x2 5 12 5 1  V  x , x , x   V  x , x , x  4 3 24 5 3  V  x2 , y4 , 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 Lx,x,yLx,x,x2 1 44 2 5на замену всех вхождений переменных на их значения уходит 12 шагов;пятый процессор132 V  y1, x2 , 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  y1, 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, y1, 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 , x1, 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  x2 , x5 , x1   V  x2 , x5 , x1     V  x , x , x   V  x , x , x  3 1 44 5 3 Lx,y,xLx,x,x2 1 54 2 5на замену всех вхождений переменных на их значения уходит 10 шагов.Таким образом, на выполнение п.

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

Следующей рабочей формулой являетсяV  x3 , x1 , y3  (1 шаг), для неѐ потенциально контрарной формулой являетсяV  x3 , x1, x4  (4 шага).133Для третьего процессора берем новую рабочую формулу V  x4 , y4 , x2  (1шаг). Выбираем для третьего процессора новую потенциально контрарнуюформулу V  x4 , x3 , x2  (5 шагов).Для четвертого процессора кандидатами на новую рабочую формулуявляются V  x1 , y 4 , x5  , V  x2 , y4 , x5  и L x2 , x1, y4  (3 шага).

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

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