<<
>>

3.4.Описание алгоритма поиска вывода в системе BMV

Алгоритм описывается следующим образом.

- Сначала задаются основные процедуры алгоритма. Описываются их особенности и порядок применения.

- Далее описывается механизм меток: объясняется, когда и на какие формулы и цели ставятся (снимаются) метки.

- Затем следует пошаговое описание алгоритма поиска вывода в системе BMV.

Пусть ПВ и ПЦ служат сокращениями для понятий «последовательность вывода» и «последовательность целей», соответственно, тогда к формулам из ПВ применяются следующие процедуры, которые мы делим на три группы: процедуры 1*- 4*, которые применяются только к формулам из ПВ; процедура 5*, которая применяется только к целям из ПЦ, и процедуры 6*-7*, которые применяются как к формулам из ПВ, так и к целям из ПЦ.

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

Задается следующий порядок применения: пропозициональные правила (в произвольном порядке) применяются в первую очередь. Среди кванторных правил первым применяется —3и. Затем применяется 3и.

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

Пропозициональные правила vhи ⊃hприменяются следующим образом:

h.Пусть А2⊃В ∈ПВ и формула А2⊃В не отмечена меткой М0 (смысл данной метки см. далее).10 Если среди всех неисключенных формул в ПВ найдется формула А1: А^ = А^, где θ - унификатор, и ни одна переменная не ограничивает сама себя, то данный унификатор применяется к А2⊃В, А1 и из формул А^, А2⊃Вθ по правилу ⊃hвыводима формула Вθ.

vh.Аналогично ⊃h.

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

Синтетические правила введения применяются следующим образом:

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

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

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

в. Пусть цель противоречие является текущей целью в ПЦ. Если среди неисключенных формул из ПВ найдутся формулы А и —В: АО = ВО, где θ - унификатор, и ни одна переменная не ограничивает сама себя, то к последней неисключенной посылке С из ПВ применяется правило — в, формула —С добавляется в ПВ, все неисключенные формулы из ПВ, начиная с формулы С и заканчивая формулой, предшествующей формуле —С, исключаются из ПВ, а цель противоречие помечается как достигнутая.

b.Пусть формула ЗαА(α) является текущей целью в ПЦ. Если среди неисключенных формул из ПВ найдется формула А(1), где t - произвольный терм, то к формуле /\(t) применяется правило Зв, формула ЗαА(α) добавляется в ПВ, а цель ЗαА(α) помечается как достигнутая.

Vb.Пусть формула VαА(α) является текущей целью в ПЦ. Если среди неисключенных формул из ПВ найдется формула А^), где αiне является абсолютно

10 Грубо говоря, к формуле А2⊃В не применялось правило ⊃h.

ограниченной переменной, то, если ни одна переменная не ограничивает сама себя при абсолютно ограниченной αi, к формуле A(αi) применяется правило Vb,формула VαA(α) добавляется в ПВ, делается отметка, что αi относительно ограничивает все остальные свободные переменные в A(αi), а цель VαA(α) помечается как достигнутая.

Процедура 3*определяет применение вц-правил, кроме V∣.ll.[9]Aлгоритм ищет первую сверху вниз сложную неисключенную формулу из ПВ, которая не отмечена метками М0 или М5 (смысл этих меток см. далее). Эта формула является вц-формулой. Вид вц-формулы определяет, какое именно вц-правило применимо.

Процедура 4*применяется после всех остальных процедур, если в ПВ содержатся неисключенные формулы вида VαA(α), к которым уже применялось правило Vи (т.е. они отмечены меткой М1). В таком случае метка М1 снимается со всех таких формул квантор общности снимается по некоторым определенным термам из ПВ [10]

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

К формулам из ПЦ применяются следующая процедура:

Процедура 5*определяет применение ц-правил.

Ц-правила применяются к текущей цели следующим образом:

&ц. Пусть формула A &В является текущей целью в ПЦ. Если она не достижима, то формула A становится текущей целью и отмечается меткой М3. Если цель A достижима, то текущей целью становится формула В. Если цель В достижима, то текущей целью вновь становится формула A &В.

v4. Пусть формула A v В является текущей целью в ПЦ. Если она не достижима, то формула A становится текущей целью и отмечается меткой М4. Если цель A недостижима, то цель A удаляется из ПЦ и формула В становится текущей целью и отмечается меткой М5. Если цель В недостижима, то цель В удаляется из ПЦ, формула —(A &В) помещается в ПВ в качестве последней посылки и цель противоречие становится текущей целью.

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

—ц. Пусть формула А является текущей целью в ПЦ, где А может быть либо элементарной формулой P(α), либо —C, либо C v D, либо 3αC. Если она не достижима, то формула —А помещается в ПВ в качестве последней посылки и цель противоречие становится текущей целью.

Зц. Пусть формула ЗαА является текущей целью в ПЦ. Если она не достижима, то формула А^ф), где β - новая неабсолютная переменная, становится текущей целью.

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

По всему дереву поиска вывода применяется следующие процедуры:

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

Процедура 7*осуществляет с помощью алгоритма унификации проверку достижимости текущей цели.

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

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

Важную роль в работе алгоритма играет механизм меток.

S Следующие метки ставятся на формулы из ПВ:

М0 - ставится на посылку (в однопосылочных) или на большую посылку (в двухпосылочных) правила исключения после применения данного правила.

М1 - ставится на формулы вида VαA после применение к ним правила Vh.

М2 - ставится на формулы, полученные в результате применения правил исключения.

Ό Следующие метки ставятся на цели из ПЦ:

М3 - ставится на левый конъюнкт Ai, полученный из цели Ai&Aj.

М4 - ставится на левый дизъюнкт Ai, полученный из цели Aiv Aj.

М5 - ставится на правый дизъюнкт Aj, полученный из цели Ai v Aj.

М6 - ставится на формулу A(t), полученную из цели 3αA(α).

S М7 - ставится на формулы из ПВ и ПЦ при применении вц-правил.

Описание алгоритма

Символами /... / обозначены комментарии.

1. Определяется главная цель вывода. Таковой является формула, стоящая справа от знака выводимости в заданном утверждении о выводимости. Данная формула помещается в качестве текущей цели в ПЦ. Если слева от знака выводимости стоят формулы, то все они помещаются в качестве начальных посылок в ПВ. Все свободные переменные из текущей цели и начальных посылок помечаются как абсолютно ограниченные. Переход к 10. Мотори™ проверяет, не является ли рассматриваемый вывод тривиальным, т.е. главная цель вывода унифицируется с одной из начальных посылок вывода./

2. Применение правил исключения к формулам из ПВ.

2.1. Применяется процедура 1*. /Применяются правила исключения./

При этом на посылки правил вывода вида A & В, A v В, A ⊃В, ——A, —(A v В), —3α A, VαA и 3αA, к которым были применены, соответственно, правила &и, vh, ⊃h,— и, —v4, —3и, V4и 3и, ставится М0, указывающая на два обстоятельства: (а) недопустимость вторичного применения к ним указанных правил, (б) невозможность их использования в качестве вц-формул. На заключения правил вывода ставится М2.

Правила 3и, V4применяются следующим образом:

Vh.

a) Квантор общности снимается по правилу V. с формулы VαА по новой неабсолютной переменной. На формулу VαА ставится метка М1.

b) Если вхождение квантора V по переменной α в формуле А вырождено, то результатом снятия квантора V будет А.

Зи.

a) Квантор З снимается по правилу Зи с формулы ЗαА по новой абсолютной переменной.

b) Рядом с так полученной формулой А^ф) пишется "β - абс., γ1, γ2,..., γn- огр.", где γ1, γ2,..., γn- все свободные переменные, входящие в ЗαА.

c) Если первое вхождение квантора З по переменной α в формуле ЗαА вырождено, то результатом снятия квантора З будет А.

Переход к 10.

2.2. Если ни одно правило исключения не применимо, то переход к 3.

3. Применяется процедура 5* к текущей цели A.

• A - элементарная формула P(α). Переход к 4.

• Главный знак A--- 1. Переход к 4.

• A = Ai⊃Aj. Переход к 5.

• A = Ai&Aj. Переход к 6.

• A = AiV Aj. Переход к 7.

• A = ЗαА. Переход к 8.

• A = VαА. Переход к 9.

• A есть ⊥. Переход к 12.

4. Формула —А помещается в ПВ в качестве последней посылки. Текущей целью становится получение ⊥. Переход к 2. ^Алгоритм начинает доказывать формулы от противного .∕

5. Формула Ai помещается в ПВ в качестве последней посылки. Текущей целью становится Aj. Переход к 2. /Алгоритм, доказывая импликативную формулу, берет в качестве посылки ее антецедент и пытается вывести ее консеквентУ

6. Текущею целью становится формула Ai. На формулу Аіставится метка М3. Переход к 10.

6.1. С формулы А; из ПЦ снимается метка М3. Текущей целью становиться формула Aj. Переход к 10.

7. Текущею целью становится формула A;. На формулу А; из ПЦ, ставится метка М4. Переход к 10.

7.1. Удаляем цель А;, отмеченную М4. Текущей целью становиться формула Aj. На формулу А.) ставится метка М5. Переход к 10.

7.2. Удаляем цель А.), отмеченную М5. Текущей целью становиться ⊥. Формула — (A; V Aj) помещается в ПВ в качестве последней посылки. Переход к 2.

8. Текущей целью становиться формула А^у), где v - новая неабсолютная переменная. На формулу А^у) ставится метка М6. Переход к 10.

8.1. Удаляем цель А^у), отмеченную М6. Текущей целью становиться ⊥. Формула —ЗαА(α) помещается в ПВ в качестве последней посылки. Переход к 2.

9. Текущей целью становиться формула А^ф), где β - новая абсолютная переменная.

a) Отмечается, что «β - абс., γ1, γ2,..., γn- огр.», где γ1, γ2,..., γn- все свободные переменные, входящие в VaА.

b) Если первое вхождение квантора V по переменной α в формуле VaА(a) вырождено, то результатом снятия квантора V будет сама формула А.

Переход к 10.

10. Применяется процедура 7*.

10.1. Текущая цель достигнута. Применяется процедура 6* (глобальная подстановка):

• Если текущая цель отмечена М3, то переход к 6.1. /Начинаем доказывать правый конъюнктУ

• Если текущая цель не отмечена М3, то переход к 11.

10.2. Текущая цель не достигнута:

• Если текущая цель отмечена М4, то переход к 7.1. /Начинаем доказывать правый дизъюнктУ

• Если текущая цель отмечена М5, то переход к 7.2. /Начинаем доказывать дизъюнкцию от противногоУ

• Если текущая цель отмечена М6, то переход к 8.1. Начинаем доказывать цель ЗαА(α) от противногоУ

• Если текущая цель не отмечена М4-М6, то переход к 3.

11. Достигнута текущая цель An.

11.1. Если An- главная цель, то Anустраняется из ПЦ. Выход из алгоритма

- вывод построен.

11.2. Если Anне является главной целью, то

Если Anесть ⊥, то:

a) An устраняется из ПЦ.

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

c) Делается отметка, что все формулы, начиная с формулы C и заканчивая формулой, предшествующей —С, исключаются из дальнейших шагов вывода.

d) Если в число этих формул попадает формула с меткой М2, то с соответствующей формулы снимается метка М0. Переход к 2.

Если Anне есть ⊥, то рассматриваем подцель An-1из ПЦ. В зависимости от вида An-1 рассматриваются следующие случаи:

- An-1 = AnV Akили AkV An, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула An-1, которая является результатом применения правила vbк формуле An (Ak).

c) На формулу An V Ak или Ak V An из ПВ ставится метка М0.

d) Если на An-1стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

- An-1 = Ak ⊃An, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и к формулам из ПВ применяется правило ⊃b,результатом применения которого является формула Ak⊃An, где Ak - последняя неисключенная посылка в ПВ.

c) Делается отметка, что все формулы, начиная с Akи заканчивая формулой An, исключаются из дальнейших шагов вывода.

d) Если в число этих формул попадает формула с меткой М2, то с соответствующей формулы снимается метка М0.

e) Если на цели An-1стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

- An-1 = Ak &An, то:

a) Anи An-1устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула An-1, которая является результатом применения правила &в к формулам Anи Ak.

c) На формулу Ak &An из ПВ ставится метка М0.

d) Если на цели An-1стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

- An-1 = VαA, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула An-1, которая является результатом применения правила Vbк формуле A(α∕β, γ1, γ2,..., Yn).

c) Делается отметка, что β абсолютно ограничена и γ1, γ2,..., γnотносительно ограничены.

d) На формулу VαA ставятся метки М0 и М1.

e) Если на цели An-1стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

- An-1 = 3αA, то:

a) An и An-1 устраняются из ПЦ.

b) Текущей целью становится предыдущая цель и в ПВ включается формула An-1, которая является результатом применения правила 3в к формуле A(α∕β).

c) На формулу 3αA ставится метка М0.

d) Если на цели An-1стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

- An-1 = ⊥, то:

a) An устраняется из ПЦ.

b) Текущей целью становится предыдущая цель An-1.

c) Если на цели An-1стояла метка М7, то с соответствующей вц-формулы снимается метка М7. Переход к 2.

12. Применяем процедуру 3*.

12.1. Если в ПВ имеются сложные формулы, не отмеченные метками М0 или М7, то к ним применяются следующие процедуры:

a) Если в выводе имеется формула вида Ai⊃Aj, то в качестве текущей цели берется Ai. Формула Ai⊃Aj и текущая цель Aiпомечаются меткой М7. Переход к 3.

ТИмея в выводе формулу вида Ai⊃Aj, алгоритм пытается вывести Aiдля того, чтобы в случае успеха применить dh∙∕

b) Если в выводе имеется формула вида Ai V Aj, то в качестве текущей цели берется — Ai. Формула Aiv Aj и цель — Aiпомечаются меткой М7. Переход к 3. ^Имея в выводе формулу вида Aiv Aj, алгоритм пытается вывести — Aiдля того, чтобы в случае успеха применить vu∙∕

c) Если в выводе встречается формула —Ai, где Aiне имеет вида Anv Ak, ЗαА, то в качестве текущей цели берется Ai. Формула — Aiи цель Aiпомечаются меткой М7. Переход к 3. ∕K формулам вида —(Anv Ak), —ЗαА применяются, соответственно, правила исключения —vu,—Зи. К остальным формулам вида —Aiалгоритм применяет вц-правила для того, чтобы получить цель противоречиеУ

12.2. Если все сложные формулы в ПВ отмечены М0 или М7, то 13.

13. Завершение алгоритма.

13.1. Если ПВ не содержит формул, отмеченных М1, то выход из алгоритма: ПВ содержит конечный контрпример. ТЕсли в выводе нет формул вида VαA(α), то ПВ содержит конечный контрпример (опровержение) для данной выводимости7

13.2. В противном случае переход к 14.

14. Применение процедуры 4*. ТПрименение Vb4∙∕

Квантор общности снимается по правилу V4с каждой неисключенной формулы вида VαA из ПВ по некоторым определенным термам из ПВ. Со всех формул вида VαA снимается метка М1. Переход к 10.

Конец описания.

Приведем пример работы алгоритма. (Курсивом мы будем обозначать текущую цель.)

Пусть необходимо обосновать в алгоритме вывод формулы VxP(x) &VxQ(x) из формулы Vx(P(x) &Q(x)).

Согласно пункту 1 описания алгоритма, формула VxP(x) &VxQ(x) помещается в ПЦ в качестве главной цели, а последняя формула Vx(P(x) & Q(x)) помещается в ПВ в качестве начальной посылки. Aлгоритм переходит к проверке достижимости текущей цели.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) &Q(x)) - посылка VxP(x) &VxQ(x)

Т. к. текущая цель не достижима, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Согласно пункту 3, текущей целью становится левый конъюнкт, на который ставится метка М3.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) & Q(x)) - посылка VxP(x) &VxQ(x)

VcP(x)m3

Т.к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Согласно пункту 3, текущей целью становится формула P(x∕y1), где y1- это новая абсолютная переменная в ПВ и ПЦ.

Теперь вывод выглядит следующим образом:

ПВ ПЦ

1. Vx(P(x) &Q(x)) - посылка VxP(x) &VxQ(x)

VxP(x)m3

P(yι), y1новая абсолютная переменная

Т.к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Поскольку текущая цель - это элементарная формула, то,

согласно пункту 3, формула —P(y1) помещается в ПВ в качестве последней посылки, а текущей целью становится ⊥.

Теперь вывод выглядит следующим образом:

Т.к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Поскольку текущая цель - это ⊥, то, согласно пункту 2, алгоритм ищет возможность применения правил исключения в ПВ. К формуле Vx(P(x) &Q(x)) применяется правило Vhпо новой неабсолютной переменной из ПВ и ПЦ, т.е. по переменной x1. На формулу Vx(P(x) &Q(x)) ставится метка М1. На формулу P(x1) &Q(x1) ставится метка М0.

Теперь вывод выглядит следующим образом:

Согласно пункту 2, алгоритм делает все возможные заключения по правилам исключения и применяет правило &и.

Теперь вывод выглядит следующим образом:

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

,P(y1) и P(x1), для которых существует унификатор {x1∕y1}), то, согласно пункту 10.1, применяется глобальная подстановка {x1∕y1} в ПВ и ПЦ. Цель ⊥помечается как достигнутая и устраняется из ПЦ, а текущей целью становится P(y1). В ПВ применяется правило — в к формулам 2, 4 и из ПВ исключаются формулы 2-5.

Теперь вывод выглядит следующим образом:

После применения —и к формуле 6 вывод выглядит следующим образом:

Поскольку текущая цель достигнута, то, согласно пункту 10.1, цель P(y1)

помечается как достигнутая и устраняется из ПЦ, а текущей целью становится VxP(x).

Теперь вывод выглядит следующим образом:

6. ——P(yOM0—⅛: 2, 4

7. P(y1)M2- —.: 6

Поскольку текущая цель является подцелью достигнутой цели, то она также является достигнутой, согласно пункту 11.2. К формуле P(y1) из ПВ применяется правило Vb,в ПВ помещается формула VxP(x), цель VxP(x) помечается как достигнутая и устраняется из ПЦ, метка М3 снимается, а текущей целью становится VxP(x) &VxQ(x).

Теперь вывод выглядит следующим образом:

Поскольку текущая цель является подцелью достигнутой цели, отмеченной меткой М3, то текущей целью становится VxQ(x).

Теперь вывод выглядит следующим образом:

Т.к. в ПВ нет формулы, которая унифицируется с VxQ(x), то, согласно пункту

3, текущей целью становится Q(y2), где y2новая абсолютная переменная в выводе.

Т.к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Поскольку текущая цель - это элементарная формула, то, согласно пункту 3, формула — Qty2) помещается в ПВ в качестве последней посылки, а

Т.к. текущая цель не достигнута, алгоритм, согласно пункту 10.2, переходит к анализу текущей цели. Поскольку текущая цель - это ⊥, то, согласно пункту 2,

алгоритм ищет возможность применения правил исключения в ПВ. К формуле Vx(P(x)

&Q(x)) не применяется правило Vh,т.к. эта формула отмечена меткой М1. Правило Vh

применяется к формуле VxP(x), в ПВ помещается формула А^), где x2- новая неабсолютная переменная в ПВ, и на формулу VxP(x) ставится метка М1.

Поскольку ни одно правило исключения не применимо, то Процедура 4* применяется следующим образом:

С формулы Vx(P(x) &Q(x)) квантор общности снимается по всем абсолютным переменным из ПВ: y1и y2, т.к. ни формула P(y1) &Q(y1), ни формула P(y2) &Q(y2) не находятся неисключенными в ПВ. На формулы P(y1) &Q(y1) и P(y2) &Q(y2) ставятся

метки М0 и М7. С формулы Vx(P(x) & Q(x)) снимается метка М1.

С формулы VxP(x) квантор общности снимается только по абсолютной переменной y2, т.к. формула P(y1) находится неисключенной в ПВ. На формулу P(y2) ставятся метки М0 и М7. С формулы VxP(x) снимается метка М1.

Теперь вывод выглядит следующим образом:

исключения и применяет правило &и к формулам 11 и 12.

Теперь вывод выглядит следующим образом:

Aлгоритм проверяет достижимость текущей цели. Поскольку она достигнута

(в ПВ имеются формулы —Q(y2) и Qty2)), то цель ⊥помечается как достигнутая и устраняется из ПЦ, а текущей целью становится Q(y2). В ПВ применяется правило —в к формулам 9, 17 и из ПВ исключаются формулы 9-17.

Теперь вывод выглядит следующим образом:

После применения —и к формуле 18 вывод выглядит следующим образом:

Поскольку текущая цель достигнута, то, согласно пункту 10.1, цель Q(y2 помечается как достигнутая и устраняется из ПЦ, а текущей целью становится VxQ(x).

Теперь вывод выглядит следующим образом:

Поскольку текущая цель является подцелью достигнутой цели, то она также является достигнутой, согласно пункту 11.2. К формуле Qty2) из ПВ применяется правило Vb,в ПВ помещается формула VxQ(x), цель VxQ(x) помечается как достигнутая и устраняется из ПЦ, а текущей целью становится VxP(x) &VxQ(x).

Теперь вывод выглядит следующим образом:

Поскольку текущая цель является подцелью достигнутой цели, то она также является достигнутой, согласно пункту 11.2. К формулам 8 и 20 применяется правило

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

Еще по теме 3.4.Описание алгоритма поиска вывода в системе BMV:

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