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

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

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

Процедура отождествленияпеременных с константами в списке Г согласно системе S состоит в замене вовсех формулах списка Г переменных u1,..., u p на их значения в решении σ.Врассматриваемомслучаепроцедураотождествленияформулрассматриваться не будет, так как переменных d1,..., d m и c1,..., cm нет.Далее в [61] была определена процедура преобразования списков формул вF-наборы.

В рассматриваемом случае первый пункт этой процедуры не надовыполнять, так как любой список допустим. Четвертый пункт тоже, очевидно,выполнять не надо, а пятый при отсутствии четвертого дублирует второй, такимобразом, процедура преобразования списков формул в F-наборы принимает вид.Процедура преобразования списков формул в F-наборыПустьГ–списокформулвидаDi a1,..., ak , x1,..., xn  .

Процедурапреобразования списка Г в F-набор состоит в удалении повторений формул в этомсписке.45В нашем случае эта процедура склейки формул в F-наборах из [61]использоваться не будет, так как не используется процедура отождествленияформул.Процедура построения замкнутого F-набораПустьвформулахDi a1,..., ak , t1,..., t s и D j a1,..., ak , v1,..., vs  t1 ,..., t s–переменные, a1 ,..., a k – константы.

Обозначим первую формулу посредством А,вторую – В. Предположим, что в А входит в качестве дизъюнкции атомарнаяформула Pt1,..., ts  , в В – отрицание формулы Pa1,..., as  , то есть P a1,..., as  ,где Р – s-местный предикат. Процедура построения замкнутого F-набора по парамформул А, Pt1,..., ts  и В, P a1,..., as  , состоит в последовательном выполненииследующих действий:1.Применить к списку формул(А, В) процедуру отождествленияпеременных с константами согласно системе уравнений в переменных t1  a1  .t  as s2.Вслучаеуспешногозавершенияпроцедурыотождествления,применить процедуру преобразования полученного списка формул в Fнабор.Определение 2.1.4. F-набор будем называть замкнутым, если он можетбыть получен в результате применения процедуры построения замкнутого Fнабора к подходящим парам формул А, Pt1,..., ts  и В, P a1,..., as  .1 21 2В нашем случае, ввиду отсутствия переменных d1 , d1 ,..., d1 ,..., d m , d m , ,..., d m, правило Б имеет вид, приведенный ниже.46Процедура применения правила Б к F-наборамРассмотрим δ F-наборов Г1, D1 a1,..., ak , c11,..., c1n, Г , D a ,..., a , c ,..., c 1k 1n (2.1.5)где Г1,…,Гδ – списки формул вида Di a1,..., ak , x1,..., xn  .

Если какие-нибудь два изэтих наборов содержат общую переменную, переименуем еѐ на новуюпеременную. Таким способом добьемся, чтобы F-наборы (2.1.5) не содержалиобщих переменных. Применим к списку Г1,…,Гδ процедуру отождествленияпеременных согласно системе уравнений в переменных c11  c12    c1,c1  c 2    cnn nа затем к полученному списку – процедуру преобразования списков формул в Fнаборы. Построенный таким образом F-набор Σ является результатом примененияправила Б к F-наборам (2.1.5).Так как при решении системы уравнений (2.1.4) δ F-наборов объединяютсяв один, процедура применения правила Б к рассматриваемым формуламприобретает следующий вид.Процедура применения правила Б к F-наборам.Объединим δ одночленных F-наборов (2.1.5) в один δ-членный F-набор.Таким образом, дляформул вида (2.1.1) исчисление благоприятных наборовзадается приведенными ниже правилами А, Б и правилом перестановки.Правило А.Замкнутые F-наборы являются благоприятными.Правило Б.F-наборы, на которых процедура применения правила Бзаканчивается успешно, являются благоприятными.47Правило перестановки.

Перестановка формул в благоприятном F-набореявляется благоприятным F-набором.Определение 2.1.5. F-набор называется пустым □, если все формулы,входящие в него, не имеют переменных и тавтологичны.Определение 2.1.6.F-набор называется тупиковым, если в него входитхотя бы одна формула, не имеющая переменных и являющаяся ложной или неявляющаяся ни тавтологией, ни противоречием.Теперь, на основе приведенных процедур и правил можно сформулироватьалгоритм поиска вывода для формул вида (2.1.1), использующий тактикуобратного метода.2.2. Алгоритм IMA (InverseMethodAlgorithm), использующий тактику обратногометодаНа основе приведенных процедур и правил можно сформулироватьалгоритм поиска вывода для формул вида (2.1.1), использующий тактикуобратного метода.С целью уменьшения оценки числа шагов работы алгоритма, в дополнениек идеям метода Маслова в диссертации предлагается упорядочить все формулы S a1,..., ak   Pki x1,..., xni в (2.1.1) следующим образом.1.Так как в каждой дизъюнкции  S a1,..., ak   Pki x1,..., xni имеетсявсего одна формула Pki x1,..., xni , имеющая переменные, сгруппируем в F-наборе дизъюнкции  S a1,..., ak   Pki x1,..., xni по одинаковым именампредикатных символов Pk i .

Таким образом F-набор приобретет следующийвид:48x  S a1,..., ak   Pkini... S a1,..., ak   Pki  xnih S a1,..., ak   Pkix ni... S a1,..., ak   Pki  xnih.2.Упорядочим эти группы в порядке возрастания количества вхожденийатомарных формул с переменными. Теперь F-набор приобретет следующийвид: S a1,..., ak   Pki1x ni1... S a1,..., ak   Pki1  xnih S a1,..., ak   Pki21x ni2... S a1,..., ak   Pki2  xnih2h1 штукh2 штук   h j штукx ni  h j  S a1,..., ak   Pki j  xni j... S a1,..., ak   Pki j49где h1  h2    h j и3.Формулы вj hm   .m 1S a1,..., ak  (формулы без переменных) сначаласгруппируем по именам предикатных символов, так же, как в п.

1. Внутрикаждой группы упорядочим атомарные формулы в том же порядке поименам предикатных символов, что и в п. 2. Тогда  S a1,..., ak  в каждомF-наборе приобретет вид    Pki ak  ...  Pki ak   Pki ak  ...  Pki ak  ...1 2 1 2s1 штукs2 штук   Pki ak  ...

 Pki akijjs штукОдинаковый тип упорядочения постоянных и переменных формулпозволяет значительно сократить перебор при присвоении значенийпеременным, так как можно начинать перебор с совпадения именпредикатных символов, и как только попадается другое имя прекратитьработу.4.Ищемподстановку,котораяпозволитприсвоитьзначенияпеременным в атомарной формуле с наиболее редко встречающимсяпредикатным символом.

Если таковой не находится, то формула (2.1.1) невыводима. Если подстановка найдена, то осуществляем еѐ во всехэлементарныхдизъюнкция S a1,..., ak   Pki x1,..., xni .Повторяемпроцедуру до тех пор, пока все значения переменных не окажутся замененыконстантами.В качестве обоснования п. 4 следует отметить, что, выбирая наиболее редковстречающийся символ, мы сокращаем время работы алгоритма, так какпроцесс построения вывода имеет вид дерева, в котором количествоуровней не зависит от выбора предикатного символа, но количество ветвей50на каждом уровне зависит от частоты встречаемости символа. Если ближе ккорню находится вершина с малой степенью, то общее количество вершинуменьшается.Алгоритм IMA (Inverse Method Algorithm)1.

Строим δ-членный F-набор, формулы в котором не повторяются. Тоесть в формуле (2.1.1) удаляем все знаки конъюнкций и составляем списокэлементарных дизъюнкций вида  S a1,..., ak   Pki x1,..., xni .2. Присваиваем значения переменным следующим образом:2.1. Отменяем все пометки об удалениях предикатных формул изS  (если они были).2.2. Берем формулу  S a1,..., ak   Pki t1,..., tm  из рассматриваемого Fнабора, содержащую m-местный предикатный символ такой, что набор t1,..., tmсодержит хотя бы одну переменную.2.3. Ищем вS   формулу Pki v1,..., vm  при наборе констант v1,..., vm сотрицанием перед выбранным в п. 2.2 предикатным символом. Если нашлиподходящую формулу – помечаем еѐ как удаленную и переходим к пункту 2.4,если еѐ не существует, то переходим к пункту 3.2.4.

Решаем систему уравнений, отождествляющую списки переменныхt1,..., tm и констант v1,..., vm . В случае, если эта система имеет решение1, перейти кпункту 2.5, если система решений не имеет, то перейти к пункту 2.3.2.5. Заменяем во всем F-наборе переменные из списка t1,..., tm на ихзначение, полученные в пункте 2.4.2.6. В полученном F-наборе удаляем повторения формул.2.7. Если получился пустой F-набор, то алгоритм заканчивает работу2.1Кроме указанных в определении 2.1.3 случаев, система уравнений не имеет решений, если какое-то изприсваиваемых переменным значений, было присвоено ранее другой переменной.2Положительный результат работы алгоритма можно увидеть, вернувшись назад по действиям алгоритма изапомнив все не отмененные присвоения значений переменным.512.8.

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

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