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

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

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

Здесь и далее & S   обозначает конъюнкциювсех атомарных формул из множества S   .Доказательство каждой из этих формул базируется на доказательствеформулывида & S    x A x  ,гдеA x – элементарная конъюнкция.Этаформула равносильна i 1x1,..., xn   & Di a1,..., ak , x1,..., xn (1.1.7)для любых наборов значений констант a1,..., ak ,где Di a1,..., ak , x1,..., xn  имеет вид S    Pki x .Проверкаформулы (1.1.7) будет рассматриваться в работе.26Для доказательства общезначимости формулы (1.1.7) можно использоватьразличные методы.

В частности, она выводима в секвенциальном исчислениипредикатов тогда и только тогда, когда существуют подстановки термов t1,..., tniвместо переменных x1,..., xni такие, что для любого набора значений констант  вкаждом конъюнктивном члене найдется контрарная пара (то есть парадизъюнктивных членов, один из которых находится без отрицания, а второйотличается от него только наличием отрицания)[38].

Иными словами, системауравнений вида F1  P1 x1,..., x1111,..., s Fs  P1 x1,..., x1ssi  1,...,   F1  P x1,..., x111,...,sFs  P x1,..., xssимеет решение. Здесь квадратная скобка означает, что верно хотя бы одно изуравнений (система типа или), фигурная скобка означает, что верны всевнутренние системы (системы типа и), знак  использован для обозначенияграфического равенства формул.Такимобразом,& S    x Ax  леваятребуетсянайтитакиетермы t1,..., tni ,чтови правая частиявляются одним и тем же словом.Другими словами, требуется найти термы, являющиеся решениями системыуравнений следующего вида:27 1,..., s   t1  a1i  1,...,  1,..., s  tni  ani 1,..., s  где s – количество атомарных формул в  S a1,..., ak  .

Непосредственноерешение этой системы имеет экспоненциальную от длины записи формулы A x оценку числа шагов[38].1.2. Обратный метод С.Ю. Маслова для решения задач логико-предметногораспознавания образовСредиприменяющихсяметодовустановлениявыводимости,приспособленных для создания машинных алгоритмов и программ, наибольшуюизвестность получил, предложенный в 1964 г. Дж.А. Робинсоном, методрезолюций [103]. Одновременно и независимо С.Ю Масловым был предложенобратный метод, базирующийся на секвенциальном исчислении предикатов[55],такжепредназначенныйдляавтоматизацииустановлениявыводимости.Обратный метод является тщательно продуманным с точки зрения перебора.Кроме того, область применимости обратного метода шире [17], [56].

При этомобратный метод не получил широкого распространения ввиду сложностиреализации.28Общая схема обратного методаДля произвольного исчисления B со свойством подформульности ипроизвольной секвенции Σ будем строить вывод, определяя сначала структуруверхних секвенций потенциального дерева вывода, затем структуру секвенций,лежащих ниже верхних и так далее (таким образом, метод является «обратным»по сравнению с поиском «снизу вверх»). Это достигается построениемобисчисления И , благоприятных наборов[51].

Выводимыми объектами этогоисчисления (Σ-наборами) являются пары [L;B], где L – список подформулΣ, а В –система зависимостей между элементами из L (точнее, L состоит из номеровнекоторых заранее выбранных подформул Σ). Для каждой секвенции Σ’ и каждогоΣ-набора Н определяется отношение Н лежит в Σ’. Формулируются правила А и Бдля исходных и для порождаемых благоприятных наборов соответственно. Длякорректности метода достаточно выполнения двух условий:a)для каждого Σ-набора Н, порожденного по правилу А, всякая Σ’, вкоторой лежит Н, выводима в B;b)если Н порождено из благоприятных наборов поправилу Б и лежит вΣ’, то Σ’ выводима в B;При подходящем определении понятий гарантируется и полнота метода: Σвыводима в B тогда и только тогда, когда пустой Σ-набор благоприятен.Таким образом, для определения конкретизации обратного метода следуетуказать:1.алгоритм, нумерующий те подформулы из Σ, которые нужны дляопределения Σ-набора;2.язык для задания систем зависимостей;3.Правила А и Б, удовлетворяющие условиям а) и b) соответственно.29Для обеспечения «метапеременности» следует предусмотреть, чтобырезультаты применения правил А и Б лежали в большем числе секвенций.Кроме ориентированности на практический поиск вывода, обратный методобладает рядом черт, которые делают его удобным теоретическим аппаратомпостроения разрешимых классов и классов сведения.

На его основе удаетсяполучить обобщения известных результатов, найти ряд новых разрешимыхклассов, объединить единой схемой почти все имеющиеся результаты поразрешимым фрагментам классического исчисления предикатов.В [61] сформулирован обратный метод Маслова для замкнутых формул Fвида:z1,..., zk x1,..., xn  y1,..., ym  & Di z1,..., zk , x1,..., xn , y1,..., ym  i 1,где(1.2.1)Di z1,..., zk , x1,..., xn , y1,..., ym  – дизъюнкция атомарных формул и ихотрицаний 1  i    .Зафиксируем бесконечный список Ппеременных a1, a2 , a3 ,... , которые невходят в формулу F и попарно различны. Рассматриваются растущие деревья DF,которые начинаются в корне V0. Корню V0 приписывается пустой список формул.Каждому последующему узлу V дерева DF приписана формула:Di a1,..., ak , c1,..., cn , d1,..., d m  , (1.2.2)Где 1  i    , c1,..., cn – переменные из списка П, d1,..., d m – попарно различныепеременные из списка П, отличные так же от переменных a1,..., ak , c1,..., cn .Определение1.2.1[61].СписокГформулвида(1.2.2)называетсятавтологичным, если можно указать атомарную формулу Е, которая входит водну из формул списка Г в качестве члена дизъюнкции отрицание Е так жевходит в одну из формул списка Г в качестве члена дизъюнкции.30Определение 1.2.2[61].

Набор u1,..., un подходит для продолжения списка Гформул вида (1.2.2), если нельзя указать натуральное число i 1  i    и такиепеременные t1 ,..., t m ,что формула Di a1,..., ak , u1,..., un , t1,..., tm  содержится всписке Г.Определение1.2.3[61].ДеревоDFназываетсяΩ-деревомпоискадоказательства формулы Fвида (1.2.2), если для любого узла Vвыполняютсяследующие условия:если список Г(V) тавтологичен, то Vявляется листом дерева DF;если для списка Г(V) существует подходящий для продолжения набориз Ω, то из V выходит δ ребер в узлы V1 ,...,V , для всех i 1  i    узлу Viприписана формула Di a1,..., ak , u1,..., un , t1,..., tm  , где u1,..., un – первый попорядку набор из Ω, который подходит для продолжения списка Г(V);переменныеd1,..., d mпопарноразличны,отличныотпеременныхa1,..., ak , u1,..., un и не входят в формулы списка Г(V).Определение 1.2.4[61].

Ω-дерево поиска доказательства формулы Fназывают замкнутым, если оно конечно и для каждого листа V список Г(V)тавтологичен.Ω-дерево поиска доказательства формулы F однозначно определяетсяформулой F, бесконечным списком переменных П и бесконечным списком всехm-членных наборов Ω.Теорема 1.2.1[61]. Для того, чтобы формула F была выводима в исчислениипредикатов, необходимо и достаточно построить замкнутое Ω-дерево поискадоказательства формулы F.Определение1.2.5[61].Считают,чтоx<y,еслисуществуюттакиеDi a1,..., ak , u1,..., un , d1,..., d m  из списка Г, что х совпадает с одной из переменныхu1,..., un , а у – с одной из переменных d1,..., d m .31Определение 1.2.6[61].Список Г формул вида (3) называют допустимыми,если выполняются следующие условия: длякаждойформулы Di a1,..., ak , u1,..., un , d1,..., d m изспискаГформулы Di a1,..., ak , u1,..., un , d1,..., d m иa1,..., ak , d1,..., dm попарно различны; каковыбынибылиDr a1,..., ak , v1,..., vn , c1,..., cm  из Г, если dl 1  l  m совпадает с переменнойср 1  p  m  , то l=p; нельзя указать такую цепочку переменных x1,..., xl l  1 , входящих вформулы из Г, что  x1  x2  ...

 xl  x1  .Определение 1.2.7[61].Допустимый список Г формул вида (1.2.2) – Fнабор, если выполняются следующие условия:Формулы в списке Г не повторяются;Каковыбынибылиформулы Di a1,..., ak , u1,..., un , d1,..., d m иDr a1,..., ak , v1,..., vn , c1,..., cm  из списка Г, если наборы d1,..., d m и c1 ,...,cmимеютобщуюпеременную,тоDi a1,..., ak , u1,..., un , d1,..., d m иDr a1,..., ak , v1,..., vn , c1,..., cm  совпадают.Пусть 1,...,  l и 1,..., l – списки переменных и констант, которые могутсовпадать между собой и с константами из списка П. Рассмотрим системуравенств:1  1   l l(1.2.3)32Пусть u1,..., u p – список без повторений всех переменных, отличных отпеременных a1,..., ak и входящих в равенства системы (1.2.3).Определение 1.2.8[61]. Систему (1.2.3) называютсистемой уравнений впеременных u1,..., u p .Решением системы уравнений (1.2.3) называют всякийнабор переменных 1,..., pтакой, что в результате одновременной заменыпеременных u1 ,...,u p на их значения в решении 1,..., p левые и правые частикаждого равенства системы совпадут.

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

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