<<
>>

3.3.Правила поиска вывода в системе BMV

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

6

успешно решить саму задачу.

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

Особо отметим, что в данном контексте «правило» не понимается как преобразование формул в рамках некоторого исчисления (в таком смысле «правило» понимается в Главе 2 нашей работы, где речь идет о формулировке правил системы BMV).

Здесь и далее понятие «синтетическое (аналитическое) правило» понимается как некоторая эвристика, позволяющая в процессе поиска вывода выводить новые

формулы из уже имеющихся (синтетические правила) или сводить задачу поиска некоторой формулы к подзадачам поиска других формул (аналитические правила).

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

7 семантической полноте алгоритма поиска натурального вывода.

Все правила вывода системы BMV рассматриваются как синтетические правила поиска вывода в этой системе. Действительно, правила введения и правила исключения логических связок обладают общей чертой: с их помощью в последовательность вывода (ПВ) добавляются новые формулы. Таким образом, в процессе поиска вывода эти правила используются для выведения новых формул в ПВ.

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

Остановимся более подробно на последовательности целей.

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

Другим важным понятием для ПЦ является понятие «достигнутой цели». Если текущей целью является формула, то текущая цель достижима (достигнута), если она унифицируется с некоторой неисключенной формулой из ПВ.

Если текущей целью является противоречие, то текущая цель достижима (достигнута), если в выводе содержатся две неисключенные формулы вида A и —В,

7 В противном случае, множество аналитических и синтетических правил, заданных в смысле Главы 2 нашей работы, в совокупности с некоторым понятием вывода образовывало бы некоторое промежуточное исчисление, позволяющее искать вывод в системе BMV. См. данный подход в [Sieg], [Sieg &Byrnes].

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

В противном случае цель считается недостижимой (недостигнутой).

Понятие «недостижимая (недостигнутая) цель» следует понимать в том смысле, что данная цель недостижима в результате одного конкретного действия алгоритма унификации.

Таким образом, цель может быть недостижимой в какой-то определенный момент построения вывода, но может стать достижимой в каком-то следующем моменте построения вывода.

Теперь остановимся подробнее на аналитических правилах поиска вывода.

Характерной чертой этих правил является сведение «задачи поиска некоторого вывода к одной или нескольким подзадачам по поиску вспомогательных выводов» [Смирнов и др., с. 4]. Используя предложенную в нашей работе терминологию, можно сказать, что аналитические правила суть переходы от текущей цели к подцели, которая, в свою очередь, сама становится текущей целью. Соответственно, цель, из которой получена подцель, называется предыдущей целью.

Например, необходимо достигнуть цель А &В. Мы можем достигнуть А &В с помощью BMV-правил из имеющихся в выводе посылок. Однако поиск вывода существенно облегчается, если применить к текущей цели А &В некоторое аналитическое правило и получить подцели А и В, из которых А становится текущей целью, а В - предыдущей целью по отношению к А (и подцелью по отношению к А &В) в ПЦ. Если подцели А и В достижимы (а значит, А и В находятся в ПВ), то, применяя &в, можно достигнуть цель А &В.

Если необходимо достигнуть текущую цель А ⊃В, то можно взять формулу А в качестве посылки в ПВ и стараться достигнуть подцель В. Если подцель В достижима (а значит, В находится в ПВ), то, применяя ⊃b,можно достигнуть цель А ⊃В.

Если необходимо достигнуть текущую цель —А, то лучше взять в качестве посылки формулу А в ПВ и стараться достигнуть подцель противоречие. Если подцель противоречие достижима, то, применяя —в, можно достигнуть цель —А.

Такие советы по поиску вывода иногда называются эвристиками. Общее для вышеперечисленных эвристик состоит в том, что благодаря их использованию

достижение цели сводится к достижению одной или нескольких подцелей. При этом степень подцелей меньше, чем степень цели.[7]

В нашей работе мы называем такие аналитические правила поиска вывода для целей ц-правилами.

В алгоритме задаются следующие ц-правила с использованием меток М3-М6 (смысл меток приводится ниже, в описании алгоритма).

В правиле —ц формула А может быть либо элементарной формулой P(α), либо —C, либо C V D, либо ∃αC.

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

Правило Vц позволяет от цели VαA(α, γ1,., γn) перейти к подцели A(α∕β, γ1,., γn), где β - абсолютно ограниченная переменная и γ1,., γnотносительно ограничены. Если подцель A(α∕β, γ1,., γn) достигнута (т.е. в ПВ имеется формула В: В и A(α∕β, γ1,., γn) унифицируемы с помощью подстановки Ω), то к ВО можно применить правило Vbпо переменной β, вывести формулу VαA(α, γ1,., γn)Ω и достигнуть цель VαA(α, γ1,., γn)Ω.

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

правила не работают с целью противоречие. Значит, сформулируем простое свойство ц- правил: процесс сведения произвольной цели из ПЦ с помощью ц-правил к цели противоречие конечен. Содержательно это означает, что процесс сведения некоторой цели к цели противоречие с помощью ц-правил конечен.

Помимо ц-правил, существуют группа аналитических правил поиска вывода, которые применяются не к целям из ПЦ, а к формулам из ПВ.

Например, пусть текущей целью является противоречие, она не достигнута и в ПВ имеется формула A ⊃В. Тогда применяем к A ⊃В некоторое аналитическое правило поиска вывода и текущей целью становится формула A.

На первый взгляд, необходимость данного правила поиска вывода неясна: каким образом достижение (причем, A не всегда достижима) цели A связано с достижением цели противоречие?

Однако, если мы сможем достигнуть цель A, то, применив ⊃mк A ⊃В и A, получим в ПВ формулу В. Наличие в ПВ формул A и В, наряду с формулой A ⊃В, облегчает достижение цели противоречие. Поиск цели A играет важную роль и тогда, когда цель A недостижима: именно поиск A тогда, когда в ПВ имеется A ⊃В, позволяет говорить, что ПВ содержит контрпример, опровергающий данную выводимость (этой темы мы подробно касаемся в следующей главе нашей работы).

Если необходимо получить цель противоречие, когда в ПВ имеется формула A V В, то применяем к A v В некоторое аналитическое правило поиска вывода и текущей целью становится формула —A. Если —A достижима, можно применить vи к формулам A V В, — A и получить формулу В. Если не удается достигнуть цель — A, то ее поиск способствует построению контрпримера.

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

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

В правиле —вц формула А не имеет вида элементарной формулы P(α), или C v D, или 3αC.

В правиле Vbhтерм t не может быть неабсолютной переменной. Более того, мы подставляем только такой терм t, что неисключенная формула Λ(α∕t) не находится выше в ПВ.[8]

Отметим, что правило Vbhотлично от правила Vh.Правило Vbhразрешает снимать квантор общности по некоторым определенным термам из ПВ. Таким образом, применение правила Vbhпредставляет собой конечное число применений правила Vh.

ВЦ-правилам соответствуют аналитические правила удаления в [Смирнов и др.], [Смирнов-мл.] и [Смирнов-мл.1]. Сравнительный анализ данных групп правил обнаруживает значительные различия. Например, в нашей нотации аналитическое правило поиска вывода v_ae в [Смирнов-мл., с. 99] запишется следующим образом:

Если мы хотим достичь текущей цели C из формулы А v В, то мы помещаем А в ПВ в качестве посылки и в качестве текущей цели берем формулу С. Если С достижима, то формула В помещается в ПВ в качестве посылки и текущей целью становится формула С. Если и в этом случае С достижима, то в ПВ применяется правило разбора случаев.

В системе BMV нет правила разбора случаев. Поэтому предлагаемый алгоритм в такой ситуации берет в качестве текущей цели —А. Если она достижима, то к формулам А v В, —А из ПВ применяется правило vuи в ПВ помещается формула В.

Отметим, что формульным коррелятом правила v_ae является отношение между формулами (А v В) С и (A ⊃C) &(В ⊃С). Данное отношение является отношением логического следования в обе стороны, т.е. эти формулы эквивалентны в

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

В свою очередь, формульным коррелятом правила vb4является отношение между формулами (Λ V В) ⊃С и (—Λ ⊃В) ⊃С, которое также является отношением логического следования в обе стороны, т.е. эти формулы эквивалентны. Таким образом, правило v∣.llпредставляет собой иной эквивалентный переход.

Λналогичные замечания относятся к аналитическому правилу поиска вывода —_ae в [Смирнов-мл., с. 99], которое в нашей нотации запишется следующим образом:

Если мы хотим достичь текущей цели C из формулы Λ ⊃В, то мы помещаем —С в ПВ в качестве посылки и в качестве текущей цели берем формулу Λ. Если она достижима, т.е. формула Λ появилась в ПВ, то к формулам Λ ⊃В, Λ применяется правило зи и в ПВ помещается формула В. При этом текущей целью становится формула С.

Предлагаемый алгоритм в такой ситуации устанавливает текущую цель Λ. Если она достижима, то к формулам Λ ⊃В, Λ применяется правило ои и в ПВ помещается формула В.

Формульным коррелятом правила —_ae является отношение между формулами (Λ В) С и (—С ⊃Λ) &(В ⊃С). Данное отношение является отношением логического следования в обе стороны, т.е. эти формулы эквивалентны в классической пропозициональной логике. Таким образом, правило —_ae представляет собой эквивалентный переход. Однако наш алгоритм в такой ситуации вводит новую текущую цель Λ, т. е. он не использует эквивалентные переходы.

Итак, алгоритм осуществляет поиск вывода в двух направлениях.

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

Второе направление - от доказываемой формулы (главной цели) к формулам вывода путем применения аналитических правил поиска вывода (ц-правил и вц- правил): к доказываемой формуле (главной цели) применяются ц-правила и к формулам из ПВ применяются вц-правила.

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

Еще по теме 3.3.Правила поиска вывода в системе BMV:

  1. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  2. Поиск определения воли
  3. В поиске мыслительного феномена повторения одинакового
  4. 2. Изложение учения ранних пифагорейцев: поиск источников концептов логики и зла
  5. 4.3.1 Мировоззрение: практическая формализация
  6. Оглавление
  7. Цели, основные понятия и композиция исследования
  8. Эврит
  9. Оглавление
  10. Терминологические и методологические проблемы
  11. Введение
  12. 3.3. Онтологические предпосылки самопознания.
  13. Физиология