<<
>>

4.2.Свойства алгоритма

Конечность длины произвольного блока устанавливается

Леммой 4.2.1.В произвольном алго-выводе каждый блок конечен.

Доказательство: полная индукция по порядковому номеру блока в алго- выводе формулы A.

Базис: n = 1.

Первой целью блока α1является A - главная цель алго-вывода.

Последовательность целей в α1конечна (свойство ц-правил). Конечная последовательность целей в α1 порождает конечное множество посылок в последовательности вывода. Количество применений правила V4в одном блоке конечно. Значит, количество применений правил исключения среди конечного множества посылок вывода конечно (свойство BMV-правил).

При этом, если хотя бы одна из подцелей блока α1 достигнута, то обязательно достигается главная цель A. Тем самым данный блок конечен, завершаясь выводом A.

Если же ни одна из целей не достигнута, то, в силу конечности последовательности вывода и последовательности целей в α1, конечен и сам α1, завершаясь целью ⊥.

Индуктивное предположение: допустим, лемма верна для i < n.

Индуктивный шаг: покажем, что лемма верна для i = n.

Пусть Xn-1обозначает множество неисключённых формул в алго-выводе для формулы А, где αn-1- последний блок с последней целью противоречие. По индуктивному предположению, α1,..., αn-1суть конечные блоки, а значит, Xn-1конечно.

Рассмотрим 2 случая в зависимости от вц-правила, по которому был получен блок αn: 1) блок αnполучен по вц-правилам vb4, ⊃b∣∣и —вц; 2) блок αnполучен по вц- правилу Увц.

Случай 1. Пусть формула Y является первой целью в блоке αnи формула Y получена по вц-правилам vb4, ⊃b∣∣и — вц.

Последовательность целей в αnконечна (свойство ц-правил). Конечная последовательность целей в αnпорождает конечное множество посылок вывода. Количество применений правила Vhв одном блоке конечно. Значит, конечно количество применений правил исключения среди конечного множества посылок вывода (по индуктивному предположению, Xn-1конечно плюс свойство правил исключения).

При этом, если хотя бы одна из подцелей блока αn достигнута, то обязательно достигается первая цель Y. Тем самым αn конечен, завершаясь выводом Y.

Если же ни одна из целей не достигнута, то, в силу конечности последовательности вывода и последовательности целей в αn, конечен и сам αn, завершаясь целью ⊥.

Случай 2. Пусть формула Y является первой формулой вывода в αn и формула Y получена по вц-правилу Увц. Последовательность целей в αnпуста, т.к. по вц-правилу Увц в последовательность целей не добавляются новые цели. Значит, в последовательность вывода не вводятся новые посылки. Количество применений правил исключения в блоке αnконечно (по индуктивному предположению, Xn-1 конечно; свойство правил исключения; количество применений правила Vhв одном блоке конечно).

Отметим, что последней целью в последовательности целей является последняя цель блока αn-1, т.е. противоречие.

Пусть формула Z является последней неисключенной посылкой в последовательности вывода при применении Увц, т.е. при порождении блока αn. Если цель противоречие достижима, то в последовательности вывода происходит

применение BMV-правила — в, появляется формула —Z и все формулы, начиная с формулы Z и заканчивая формулой —Z, исключаются из последовательности вывода. Значит, из последовательности вывода исключается также формула Y, которая в последовательности вывода находится ниже, чем формула Z.

Таким образом, данный блок конечен.

Если же ни одна из целей не достигнута, то, в силу конечности множества вывода и пустоты множества целей в αn, конечен и сам αn, завершаясь целью ⊥.

Доказано.

Разбив алго-вывод на последовательность блоков, перейдем к анализу блоков.

Определение 4.2.2.Если блок α получен в результате применения —вц, ⊃b4и vb4, то α является достигнутым (д-блоком), если α - последний блок алго-вывода и последняя цель в α достигнута. Если блок α получен в результате применения Vb4,то α является достигнутым (д-блоком), если α - последний блок алго-вывода и первая формула в α исключена.

В противном случае блок является недостигнутым.

Определение 4.2.3.Блок αnнепосредственно следует за блоком αk (k < n), если при порождении αnпоследним недостигнутым блоком является αk.

Если блок αnполучен по —вц, Vb4,то αnсильно непосредственно следует за αk. Если блок αnполучен по ⊃b4, vb4,то αnслабо непосредственно следует за αk.

Различение слабого и сильного непосредственного следования связано с тем, что если αn - д-блок и имеет место сильное непосредственное следование αn за αk, то αk также является д-блоком.

Дело в том, что в этом случае достижение первой цели αn, полученной по —вц, означает, что в последовательности формул вывода имеются формулы A (первая цель αn) и —A (посылка правила —вц), а это автоматически ведет к достижению последней цели ⊥в блоке αk. (Правило —вц применяется только, если последней целью в αk является ⊥.) При этом достижение последней цели в αkвлечет достижение первой цели в αk.

Значит, αk - д-блок.

Что касается Vb4,то, по определению д-блока, αnдостижим, если из последовательности вывода исключена первая формула A из αn. Исключение формулы A возможно только при применении — в, ⊃b;причем, формула С (последняя

неисключенная посылка в последовательности вывода), исключаемая в результате применения правил — в, ⊃b,находится выше, чем формула А. Т.к. применение правил введения детерминируется целями, в выводе достигнута последняя цель ⊥блока αk. Значит, αk- д-блок.

Если имеет место слабое непосредственное следование αnза αkи αnстанет д- блоком, то αk может не стать д-блоком.

Зададим формальное понятие поискового дерева (П-дерева) для алго-вывода.

Определение 4.2.4.Поисковым деревом является частично упорядоченное множество {α1, α2,...} блоков, распределенных по непересекающимся «уровням» следующим образом:

1. Нулевой уровень состоит из единственного блока α1, называемого начальным блоком;

2. Каждый блок i+1-го уровня соединён отрезком в точности с одним блоком і-го уровня;

3. Каждый блок α i-го уровня либо не соединён ни с одним блоком i+1-го уровня, либо соединён отрезками с несколькими блоками i+1-го уровня (эти блоки i+1- го уровня называются непосредственно следующими за блоком α);

4. Блок i-го уровня, не соединённый ни с какими блоками i+1-го уровня, называется заключительным блоком.

Структура алго-вывода представляет собою поисковое дерево (П-дерево), вершинами которого являются блоки, а ребрами - правила взятия цели по формуле вывода (вц-правила), по которым один блок получается из другого.

Между множеством алго-выводов и множеством П-деревьев имеет место следующее отношение: каждому алго-выводу соответствует единственное П-дерево; каждому П-дереву - счетное множество алго-выводов. Таким образом, понятие «П- дерево» является обобщением понятия «алго-вывод».

Приведем некоторые П-деревья и соответствующие им алго-выводы.

Пример 1.

В данном П-дереве блок №2 непосредственно следует из блока №1.

Такому П-дереву соответствует, например, следующий алго-вывод (вертикальная черта обозначает границумежду блоком №1 и блоком №2):

Пример 2.

В данном П-дереве: (а) блок №2 непосредственно следует из блока №1; (б) блок №2 является д-блоком (обозначается жирным контуром) и, значит, (с) алгоритм посредством бэктрэкинга вернулся на блок №1, который не является д-блоком.

Такому П-дереву соответствует, например, следующий алго-вывод (вертикальная черта обозначает границу между блоком №1 и блоком №2):

89

Отметим, что формула p v q отмечена меткой М0, сигнализирующей, что эта формула получена по vbиз формулы q. Значит, к этой формуле нельзя применять вц- правило vb4и помещать новую цель —p в последовательность целей.

Пример 3.

В данном П-дереве после того, как алгоритм посредством бэктрэкинга вернулся на блок №1 (блок №2 обозначен жирным контуром), был порожден блок №3, который непосредственно следует из блока №1.

Такому П-дереву соответствует следующий алго-вывод (вертикальная черта обозначает границу между блоком №1 и блоком №2 и между блоком №2 и блоком №3):

Отметим, что, как и в предыдущем примере, формула p v q отмечена меткой М0, сигнализирующей, что эта формула получена по vbиз формулы q. Значит, к этой формуле нельзя применять вц-правило vb4и помещать новую цель —p в последовательность целей.

Приведем некоторые примеры деревьев, которые не могут быть П-деревьями.

Пример 4.

Данное дерево содержит блок, из которого

непосредственно следует две

бесконечные (обозначается пунктирной линией) нити, состоящие из недостигнутых блоков.

Пример 5.

Данная схема означает дерево, содержащее нить, расположенную правее бесконечной нити.

В классической и интуиционистской пропозициональных логиках [Шангин], [Шангині], [ШангинЗ] по очереди работая со всеми ветками П-дерева, мы либо посредством бэктрэкинга вернемся на начальный блок П-дерева (и формула А тогда является доказанной), либо остановимся (и тогда формула А недоказуема). При этом множество неисключенных литералов (пропозициональные переменные и их отрицания в формуле А) образует контрпример. Таким образом, данные процедуры являются разрешающими.

Ситуация в первопорядковой логике сложнее. В силу результата А. Черча о неразрешимости классической логики предикатов, в общем случае процесс поиска вывода не может быть остановлен: мы не можем за конечное число шагов определить, доказуема ли произвольная формула или нет [Church], [Church1].

С другой стороны, Ж. Эрбран показал, что любая общезначимая формула логики предикатов доказуема за конечное число шагов [Линц], [Li]. В такой ситуации встает проблема выбора стратегии, позволяющей за конечное число шагов вывести произвольную общезначимую формулу классической логики предикатов. Такие стратегии известны: метод резолюции, метод аналитических таблиц, секвенциальные исчисления, метод семантических таблиц и др.

Aнализируя данную ситуацию, Ч. Чень и Р. Ли пишут: «Тем не менее существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима, если она на самом деле общезначима. Для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу. Принимая во внимание результат Черча и Тьюринга, это лучшее, что мы можем ожидать от алгоритма поиска доказательства» [Чень и Ли, с. 52]. Обратной стороной таких техник является «уход в бесконечность» в некоторых случаях, когда формула необщезначима.

Вообще, с точки зрения прикладной логики, доказательство полноты прувера - дело «неблагодарное». Распространена точка зрения, что пруверы (в том числе для поиска натурального вывода) создаются под решение каких-то отдельных прикладных проблем.[15] Поэтому проблема полноты для них не ставится.

В Главе 2 мы уже касались этого вопроса. Здесь подчеркнем, что процедура поиска вывода должна задаваться таким образом, чтобы гарантировать построение контрпримера (множества Хинтикки) даже в случае «ухода в бесконечность» [Hintikka1], [Sieg].

Определение 4.2.5.Линейно упорядоченная последовательность блоков α1, α2, ... называется нитью данного П-дерева, если: 1) α1- начальный блок и 2) Vαn (n > 1 и αn непосредственно следует за αn-1).

Напомним, что интуитивно алго-вывод представляется как последовательность блоков, полученных по одному из вц-правил. В такой ситуации большую роль играют формулы вывода, к которым применимы вц-правила (вц- формулы). Такими формулами являются формулы вида —A, A ⊃В, A V В, не

отмеченные меткой М0, т.е. к ним не применялись правила исключения, и формулы вида VαΛ(α). К этим и только этим формулам применяются вц-правила.

В процессе поиска вывода вц-правила применяются только к вц-формулам. Поиск вывода осуществляется путем выведения в ПВ подформул имеющихся в ПВ формул. С одной стороны, выведение подформул осуществляется с помощью правил исключения. Однако не ко всем формулам вывода применимы правила исключения. В такой ситуации, с другой стороны, при поиске вывода необходимо применять вц- правила, которые представляют собой переходы от формулы к ее подформулам.[16]

Поэтому нижеследующее определение выделяет роль таких формул в процессе поиска вывода.

Определение 4.2.6.Пусть при построении П-дерева αnявляется последним недостигнутым блоком и j - количество нитей, построенных ранее, следующих из блока αnи содержащих только д-блоки. Тогда Ejn = {G1, G2,., Gs, H1, H2,., Ht}, s ≥ 0, t ≥ 0, назовем порождающим множеством формул блока αnнити J+1, где G1, G2,., Gs, H1, H2,., Ht- все такие вц-формулы; причем, G1, G2,., Gs- формулы вида —Λ, Λ ⊃В, Λ V В, к которым не применялись правила исключения, и H1, H2,., Ht- формулы вида VαΛ(α), к которым применимо правило Vw

Множество Ejnконечно для любых конечных j, n, т.к. все блоки П-дерева конечны (лемма 4.2.1).

В свою очередь, конечность множества Ejnпозволяет эффективно определять формулу (формулы, если их несколько) наибольшей степени из Ejn.

Тогда степень множества Ejn(обозначается «g(EJn)») есть степень формулы наибольшей степени из Ejn.

Используя понятие П-дерева, опишем процесс поиска алго-вывода для произвольной формулы Λ:

1. Строим α1.

Если α1не является д-блоком, то 2;

Если α1является д-блоком, то алго-вывод для формулы Λ построен;

2. Рассматриваем множество E01 = {G1, G2,., Gs, H1, H2,., Ht},

Если s = 0, то:

если t = 0, то А недоказуема. Выход из алгоритма: последовательность формул вывода содержит конечный контрпример.

если t ≠ 0, то переход к 4.

Если s ≠ 0, то переход к 3.

3. По формуле G1из множества E01строится новый блок α2; переход к 5.

4. По формуле H1из множества E01строится новый блок α2; переход к 5.

5. Проверяется, является ли α2д-блоком.

Если да, то возвращаемся к α1.

Если нет, то рассматривается множество Е02= {G'1, G'2,., G's, H'1, H,2,..., H't}. Множество Е02 отличается от множества E01 = {G1, G2,., Gs, H1, H2,., Ht} тем, что, с одной стороны, некоторые формулы, которые входили в E01и были вц-формулами, таковыми не являются, а, с другой стороны, в последовательности вывода могут появиться новые вц-формулы, которые и войдут в Е02.

И т.д.

Грубо говоря, мы начинаем работать с самой левой нити в П-дереве.

Если блок становится д-блоком, то нить, содержащая д-блок, обрывается, в нити мы переходим на один «уровень» выше (такая процедура называется бэктрэкингом от английского «backtracking») и начинаем работать с блоком, из которого непосредственно следует д-блок.

Если этот блок не становится д-блоком, мы рассматриваем порождающее множество этого блока. Если оно пусто, то построение нити (а вместе с ней и всего П- дерева) обрывается, т.к., по определению П-дерева, мы не можем далее строить блоки, непосредственно следующие за этим блоком.

Если порождающее множество этого блока непусто, мы строим новый блок, непосредственно следующий за данным. Допускается бесконечное порождение блоков (например, по правилу Увц), каждый из которых непосредственно следует за предыдущим, т. е. допускается наличие бесконечной нити в П-дереве, а значит, бесконечных П-деревьев. Все блоки в такой нити являются не достигнутыми (иначе с помощью бэктрэкинга нить обрывается). Значит, ветвление в этой нити невозможно, что, в свою очередь, влечет единственность бесконечной нити в П-дереве.

Ветвление в П-дереве образуется следующим образом. Пусть из блока №1 следует блок №2 и блок №2 является д-блоком, тогда, по определению П-дерева, мы возвращаемся (бэктрэкинг) к блоку №1. При этом порождающее множество блока №1 непусто и сам блок №1 не является д-блоком. Значит, мы строим блок №3, который также непосредственно следует за блоком №1. Таким образом, в данном П-дереве из блока №1 непосредственно следуют два блока - блок №2 и блок №3, т.е. имеет место ветвление.

Далее мы покажем, что в П-дереве имеет место только конечное ветвление, т.е. в П-дереве не существует блока, из которого непосредственно следует бесконечное количество блоков. Таким образом, алгоритм по очереди (слева направо) просматривает все нити П-дерева.

С помощью понятия порождающего множества (Определение 4.2.6) мы исследуем взаимоотношения между формулами, которые входят в блоки, (непосредственно) следующие друг за другом в одной нити П-дерева. Тот факт, что при увеличении числа блоков в нити степень новых порождающих множеств не увеличивается, устанавливется

Леммой 4.2.7.Пусть αnнепосредственно следует за αk, k < n, и En, Ek- соответственно, порождающие множества из αnи αk, тогда g(En) ≤ g(Ek).

Доказательство: возвратная индукция по количеству n блоков,

непосредственно следующих за αk.

Индуктивное предположение: допустим, лемма верна для i < n.

Индуктивный шаг: покажем, что лемма верна для i = n.

Рассмотрим Ekи En. En(возможно) отличается от Ekновыми формулами, которые добавляются в последовательность вывода либо 1) по некоторому правилу введения, либо 2) по некоторому правилу исключения.

Рассмотрим случай 1. Пусть G ∈Ek- формула, к которой применяется некоторое вц-правило при порождении αnи M - первая цель (формула) в αn. Значит, по свойству вц-правил, g(M) < g(G). По свойству ц-правил, g(M') < g(M), где M'- произвольная (не первая) подцель из αn. Значит, g(M') < g(G).

Поскольку применение правил введения в αn детерминируется целями этого блока, g(Y) ≤ g(M), где Y - произвольная формула, полученная по правилам введения в αn. Из g(Y) ≤ g(M) и g(M) < g(G) следует g(Y) < g(G).

Рассмотрим случай 2. Если формула Y получена по некоторому правилу исключения, то g(Y) < g(X), где X - (большая) посылка этого правила и X ∈Ek.[17]

Итак, добавленные к Ekновые формулы (образующие En) имеют степень меньшую, чем степень формул из Ek. С другой стороны, из Ekв Enперешли все формулы вида VαΛ(α). Отсюда, g(En) ≤ g(Ek).

По индуктивному предположению, лемма верна для всех порождающих множеств из предыдущих блоков. Значит, g(En) ≤ g(Ek), для любых n, k.

Доказано. f 4.3.Семантическая полнота алгоритма

Доказательство теоремы о семантической полноте алгоритма состоит из следующих этапов.

- Показываем конечность ветвления в произвольном П-дереве, т.е. из некоторого блока в П-дереве непосредственно следует конечное число блоков.

- Конечность ветвления в произвольном П-дереве позволяет применить к П- дереву лемму Кенига [Konig] для определения бесконечной нити в П-дереве.

- Данная бесконечная нить создается канонически: в этой нити возможно построение модельного множества [Hintikka1].

Рассматривая П-дерево отметим, прежде всего, что в общем случае для логики предикатов оно не будет конечным, как для логики высказываний [Шангин], [Шангин1].

Лемма 4.3.1.В произвольном П-дереве за каждым блоком непосредственно следует только конечное число блоков.

Доказательство: полная индукция по степени g порождающего множества Ek из произвольного блока αk.

Мы допускаем, что за блоком αk следует бесконечное число блоков.

Базис: g = 0.

Если g = 0, то порождающее множество в αk пусто и построение новых блоков, непосредственно следующих за αk, невозможно.

Допущение неверно. Значит, за блоком αk следует конечное число блоков.

Индуктивное предположение: лемма верна для произвольного g < n.

Индуктивный шаг: лемма верна для g = n.

В П-дереве имеем блок αk, из которого непосредственно следует бесконечное количество блоков.

Согласно свойствам П-дерева, из этого факта вытекает следующее:

(1) блок с такими свойствами единственен в данном П-дереве;[18]

(2) все следующие в П-дереве за αk блоки суть д-блоки, но сам αk не является д- блоком.[19]

Из (1) и индуктивного предположения следует, что все нити в таком дереве конечны. Т. к. бесконечность длины нити в П-дереве - это результат потенциально неограниченного количества применений Vb4,то все непосредственно следующие за αk блоки не были получены по правилу Vb4.

Более того, т.к. αk остается не достигнутым блоком и все непосредственно следующие за αk блоки суть д-блоки, то между этими блоками и αk имеет место только слабое непосредственное следование,[20] т.е. для любого j, VαA(α) ∉Ejk, —A ∉Ejk, A v B ∈Ejk, A ⊃B ∈Ejk. Таким образом, для любого j, Ejkсостоит только из формул вида A V B, A ⊃B.

Пусть в E1kимеется, скажем, t формул вида A V B, A ⊃B. Допустим, что ко всем этим формулам алгоритм применяет вц-правила, порождая, таким образом, в П- дереве t блоков, которые непосредственно следуют из блока αk. Тогда в Et+1kне входят формулы из E1k.

По лемме 3.3.7, g(Ek+1) ≤ g(Ek), если в Ekвходят формулы вида VαA(α) или некоторые формулы максимальной степени из Ekперешли в Ek+1. Т.к. для любого j, VαA(α) ∉Ejk, то VαA(α) ∉Etk.

С другой стороны, мы показали, что в Et+1kне входят формулы из E1k. Отсюда g(Et+1k)

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме 4.2.Свойства алгоритма:

  1. Причастность (μ4θ∈(μς")∙
  2. ЗАКЛЮЧЕНИЕ
  3. Учение о красоте и триада благо-мудрость-красота.
  4. Терминологические и методологические проблемы
  5. Психоанализ
  6. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  7. 2.2. Исторические свидетельства о трактате «О природе космоса и души»
  8. 3.4.1. Учение о душе и видах душ.
  9. Гармоника в контексте мыслительного феномена прото­упорядочивания
  10. Научные исследования в перспективе вопроса о сущности воли
  11. Ответы к экзамену по логике,
  12. Sitz im Lebenпифагорейских псевдоэпиграфов
  13. Эврит
  14. Самообладание
  15. Идея: теоретическая формализация
  16. ГЛАВА I Псевдопифагорика