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

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

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

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

Теперь у второго процессора кандидатамина новую рабочую формулу являютсяV x3 , y3 , x4  , V x4 , x3 , y3  , V  y3 , x4 , x3  ,V  y3 , x1, x4  и L y3 , x3 , x1  (5 шагов), но для них не новых потенциально контрарныхформул (17 шагов). Переходим к п. 4, отменяем последнее применения п. 3.5 (10 шагов).Понижаем приоритет отождествления формулV  y1, y4 , y2  и V  x3 , x1, x4  до 0 (1 шаг),выбираем новую потенциально контрарную формулуV  x4 , x3 , x2  (1 шаг).У третьего процессора кандидатами новой рабочей формулой являютсяV x3 , y4 , x4  (1 шаг), и еѐ потенциально контрарной формулой являетсяV  x3 , x1, x4  (4 шага).Итого на эту итерацию потребовалось 65 шагов.Согласно п. 3.3 процессоры решают следующие системы уравнений (3шага), запоминаем текущие унификаторы (3 шага), длина фрагмента для каждого12процессора l2 1, l311  2 (1 шаг)ПРОЦЕССОРВТОРОЙТРЕТИЙy1  x4y 2  x2y4  x3y4  x1Решения процессоров противоречивы (1 шаг).153Согласно п.

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

3.5 потрачено 10 шагов.Пустой F-набор не выведен (6 шагов), но третий процессор вывелтупиковый F-набор (6 шагов), для него не найдено новых тавтологичных формул(12 шагов). Ищем новые рабочие формулы для всех процессоров.154У второго процессора новой рабочей формулой являетсяпотенциально контрарной формулой являетсяV x2 , x4 , y3  (8 шагов), иV  x2 , x4 , x1  (2 шага).У третьего процессора присвоены значения всем переменным (6 шагов).Переходим к п. 4, отменяем последнее применения п.

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

3.3 второй процессор решает следующее уравнение (1 шаг),запоминаем текущий унификатор (1 шаг), длина фрагмента для второгопроцессора l213  2 (1 шаг)ВТОРОЙПРОЦЕССОРy3  x1Согласно п. 3.5 имеем у второго процессора следующий F-набор155  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 Vx,x,xVx,x,xVx,x,x432432453  V  x , x , 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  x1 , 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 L x1, x4 , x3   L x4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 4 шага.Пустой F-набор не выведен (6 шагов), но выведен тупиковый F-набор (6шагов), для него не найдено новых тавтологичных формул (25 шагов).

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

Итого на эту итерациюпотребовалось 68 шагов.Согласно п. 3.3 второй процессор решает следующую систему уравнений (3шага), запоминаем текущий унификатор (3 шага), длина фрагмента для второгопроцессора l214  1 (1 шаг)ВТОРОЙПРОЦЕССОР156y1  x4y2  x3y4  x5Согласно п. 3.5 имеем у второго процессора следующий F-набор V  x4 , 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  x4 , x5 , x3   V  x4 , x5 , x3  V  x3 , x4 , y3   V  x1 , x2 , x3   V  x2 , x4 , x1   V  x2 , x5 , x1      Vx,x,xVx,x,xVx,x,x314432453 V  y3 , 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  y3 , 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 L y3 , x4 , x5   Lx4 , x2 , x5 на замену всех вхождений переменных на их значения уходит 10 шагов.Пустой F-набор не выведен (6 шагов).

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

У второго процессора больше нетновых потенциально контрарных формул (1 шаг), процессор заканчивает работу.Итого на эту итерацию потребовалось 46 шагов.Согласно п.3.9, переходим к п. 4.3, сравниваем все полученные длиныфрагментов li j i  1,...,6 : j  1,...,14 (55 шагов).Наибольшими из них являются l63  3 , l14  3 , l65  3 , l47  3 , l28  3 иl510  3 ,имсоответствуютдвафрагмента157L x4 , x2 , x5  & V  x2 , x4 , x1  & V  x2 , x5 , x1  (дляV  x4 , x3 , x2  & V  x4 , x5 , x3  & L x4 , x2 , x5 l63  3 ,(дляl65  3 ,l14  3иl47  3l28  3 ),исоответственно). Получены следующие два общих унификаторафрагмент 1 фрагмент 2y1  x2y2  x1y1  x2y2  x3y3  x 4y4  x5y3  x4y4  x5полученные фрагменты представлены на рисунке 4.Рис. 4.

Наибольшие общие фрагменты объектов «девять» и «четыре».Итого на решение этой задачи потребовалось 1345 шагов.иl510  3.

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

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