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

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

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

3.5 потрачено 12 шагов.Пустой F-набор не выведен (6 шагов), но первый, второй, третий,четвертый и шестой процессоры вывели тупиковые F-наборы (6 шагов). Дляпервого, второго, третьего и четвертого процессоров не найдены новыетавтологичные формулы (17 шагов у первого, третьего и четвертого процессорови 19 шагов у второго процессора). Для шестого процессора найдена одна новая V x2 , x5 , 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 3 5123(14 шагов), увеличиваем длину фрагмента l63  3 (1 шаг), запоминаем фрагментL x4 , x2 , x5  & V  x2 , x4 , x1  & V  x2 , x5 , x1  (1 шаг).

Ищем новые рабочие формулыдля этих процессоров.Для первого процессора это V  x2 , y4 , x1  (1 шаг), назначаем для неѐпотенциально контрарную формулу V  x2 , x5 , x1  (3 шага).У второго процессора присвоены значения всем переменным (6 шагов), онпереходит к п.

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

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

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

3.5 (4 шага). Для формул124V  x2 , x4 , y2  , V x2 , x5 , y2  ,V  y2 , x2 , x4  и V  x4 , y2 , x2  нет новых подходящих дляотождествления (24 шага). Берем новую рабочую формулу V  x4 , y2 , x2  (1 шаг) иподходящую для еѐ отождествления V  x4 , x3 , x2  (5 шагов).Итого на эту итерацию потребовалось 62 шага.Согласно п. 3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого333334процессора l1  2, l2  2, l3  2, l4  1, l5  1, l6  2 (1 шаг)ПРОЦЕССОРПЕРВЫЙ ВТОРОЙ ТРЕТИЙ ЧЕТВЕРТЫЙ ПЯТЫЙ ШЕСТОЙy1  x1y 2  x4y3  x 2y 3  x3y 4  x5y 2  x1y3  x 2y 2  x3y 4  x4y 4  x4Решения всех процессоров попарно противоречивы (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  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      V  x3 , x1, x4   V  x4 , x3 , x2   V  x4 , x5 , x3   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 на замену всех вхождений переменных на их значения уходит2 шага;125второй процессор  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 , 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  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 , 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 L x3 , x2 , x4   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага;третий процессор  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 , x3 , x5   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 , x3 , x5  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 3 5   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 3 5  V  x3 , x4 , 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 L x3 , x2 , x4   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 2 шага;четвертый процессор126  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  x , y , x   V  x , x , x   V  x , x , x   V  x , x , x   1 4 41 2 32 4 12 5 1  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  x2 , x4 , x1   V  x2 , x4 , x1   V  x2 , x5 , x1    V  x4 , x3 , x2   V  x4 , x5 , x3  V  x2 , 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 Lx2 , x1, y4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 12 шагов;пятый процессор 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, 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  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      Vx,x,xVx,x,xVx,x,x314432453 V  x2 , x4 , x1   V  x2 , x4 , x1   V  x2 , x5 , x1   Vx,x,xVx,x,x3 1 44 5 3Lx2 , y1, x4   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 10 шагов;шестой процессор127  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     Vx,x,xVx,x,xVx,x,x3 1 44 3 24 5 3  V  x4 , x5 , x3   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 шага.Таким образом, на выполнение п.

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

Дляшестогопроцессоранайденановаятавтологичная V x4 , x5 , 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увеличиваемдлинуфрагментаl65  3(1шаг)(24запоминаемформулашага),фрагментL x4 , x2 , x5  & V  x2 , x5 , x3  & V  x4 , x5 , x3  (1 шаг). Для второго, третьего и четвертогопроцессоров не найдены новые тавтологичные формулы (19 шагов у второго итретьего процессоров и 12 шагов у четвертого процессора). Ищем новые рабочиеформулы для этих процессоров.У первого процессора присвоены значения всем переменным (6 шагов).Переходим к п.

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

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

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