Interactive generation of new knowledge based on automatic means of logical inference

Full Text

Введение

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

Известны разные формальные аксиоматические теории [1] и средства логического вывода для автоматизации доказательства (АД) теорем, например, [2-8] и др. В данной работе для представления и обработки знаний используются логический язык L и исчисление J позитивно-образованных стандартизованных формул (пос-формул) [9, 10], хотя в метаязыке удобно использовать и традиционную терминологию ИП; далее ИП ‒ первого порядка [1] (собственные аксиомы теории первого порядка, если они есть, предполагаются в составе описания ПрО).

В отличие от АД, задача синтеза текстов новых знаний трудно разрешима с точки зрения автоматизации. В данной работе рассматривается порождение утверждений, которые не являются просто логическими следствиями известного знания, т.е. допускающими своё получение механической дедукцией следствий. Причина трудностей автоматизации синтеза текста нового знания ‒ в некорректности общей постановки этой задачи, и в первую очередь из-за трудности формализации интуитивных предпочтений специалиста в отношении ценности порождаемого знания. Не гарантируют этой ценности и такие, представимые синтаксически, критерии ценности теоремы, как высокая сложность (большая длина) доказательства или, наоборот, компактность текста теоремы (один из критериев элегантности), вхождение в тексты теоремы и её доказательства ключевых слов актуальной области исследований. С другой стороны, при использовании АД в интерактивном обучении человека уделяется больше внимания не только и не столько доказательству, как свидетельству корректности теоремы, сколько её понятности. Это может означать, например, что в задачах синтеза теорем для повышения ценности синтезируемого оно, возможно, должно быть структурировано с разбивкой на несколько утверждений (лемм и теорем) по критерию совокупной понятности. И это ‒ при том, что автоматически синтезировать тексты теорем, формально верных, не трудно (тем более, что в число таких теорем входят и простые логические следствия), что было продемонстрировано, например, в [11].

Сказанное подводит к целесообразности использования мер обеспечения содержательности синтезируемого уже в самой постановке задачи. Так, в контексте анализа знаний и конкретно в ситуации выяснения наличия некоторого свойства F анализируемой совокупности знаний, как некоторого описания ПрО, при отсутствии этого свойства может возникнуть задача формирования некоторого непротиворечивого условия H, гарантирующего наличие  F, т.е. задача синтеза теоремы $H\to \mathit{F}$(здесь  ‒ свойство, отличное от непротиворечивости, проверяемой просто средствами АД без обращения к синтезу ). Например, такая задача может возникнуть, когда выявлены одновременно непротиворечивость и недоказуемость  или когда выясняемое свойство  F состоит в следовании некоторых знаний из других, а H‒ условие, логически достаточное для наличия  F. При этом важно то, что в отличие от общей постановки задачи порождения новых знаний, трудности которой были отмечены выше, теперь текст утверждения $H\to \mathit{F}$, как нового знания, наследует содержательность исходного текста F как части нового текста.

В данной работе на основе интерактивного подхода к проблеме порождения новых знаний предлагается метод синтеза теорем $H\to \mathit{F}$. В этом методе человек выбирает версию условия H в ответ на предлагаемые ему опции со стороны средств АД. В настоящее время, несмотря на достижения в области АД, интерактивность в доказательстве теорем  тоже широко используется; причины ‒ не только в возможной недостаточности ресурсов (времени, памяти и др.), но и в полуразрешимости ИП и, возможно, в широте собственной аксиоматики, вызывающей неразрешимость теории, объемлющей ИП [1, 12-14].

В интерактивном режиме синтеза знаний важна наглядность текста в языке формализации. Используемый язык пос-формул, в силу их крупноблочности, как и крупноблочности средств обработки, облегчает восприятие текста человеком, по сравнению, например, с неестественной клаузальной формой представления и обработки знаний резолюционными решателями [5, 15]. Важно также то, что эвристическая структура знания, выраженная в естественном языке, сохраняется при переводе на язык пос-формул. В языке пос-формул формулы построены из ти́повых кванторов (ТК) при том, что в естественном языке можно видеть аналоги не обычных кванторов логического языка, а аналоги именно ТК. Действительно, в естественном языке квантификация предметных переменных (т.е. использование выражений, подобных фразам «для всех», «существует») сопровождается указанием некоторого условия, ограничивающего множество допустимых значений предметной переменной. Это условие в ти́повых кванторах именуется ти́повым условием. Такое частичное подобие пос-формул естественному языку и крупноблочность формульных преобразований в исчислении пос-формул повышают наглядность текста для восприятия и семантической оценки человеком [10, 16-18].

Понятие «ТК» введено в [19]. Частными случаями ТК являются ограниченные (специализированные) кванторы в формулировках свойств многоосновных алгебраических систем и моделей [20, 21]. Ти́повыми условиями здесь являются условия принадлежности значений кванторных переменных тому или иному множеству из некоторого семейства основных множеств. В языках многосортных логик эти множества, как сорта переменных, используются для повышения эффективности АД, проверки проектных ограничений и др. [22, 23]. Прямым обобщением ограниченных кванторов являются кванторы с ти́повыми условиями в форме принадлежности значений кванторных переменных так называемым ступеням [19], построенным из основных множеств с помощью операций декартового произведения и образования множества всех подмножеств. Дальнейшее обобщение кванторов со ступенями использовано при решении логико-алгебраических уравнений [24, 25].

Ти́пово-кванторный язык L пос-формул в так называемом стандартизованном виде (см. раздел 1) и соответствующее исчисление J были предложены автором совместно с А.К. Жерловым [9, 10]. Ти́пово-кванторное представление знаний автор использовал в предложенном им языке позитивно-образованных формул, но не стандартизованных. Автор ввёл этот язык, именуемый здесь как язык пон-формул для развития алгоритмов метода сравнения В.М. Матросова и синтеза теорем о сохранении свойств математических моделей [26-29]. Этот язык выше первого порядка и этим обеспечивалась представимость в нём, например, свойства устойчивости по Ляпунову. Язык пон-формул может быть и частично-формализованным ‒ до некоторой глубины структуры своих формул, а именно без формализации ти́повых условий.

Развиваемое здесь в языке L пос-формул исчисление J₊ для синтеза теорем выходит за рамки чисто дедуктивного подхода, реализованного в исчислении  [9, 10]. В отличие от двухместного правила резолюции [5], правило дедукции в J является одноместным, что снижает комбинаторность поиска выводов. Что касается систем АД не резолюционного типа, то типичными их недостатками являются многоместность и неединственность их правил вывода (см., например, [8]).

С логической точки зрения исчисление J₊ является дедуктивно-абдуктивным, и вывод в нём с логической точки зрения достоверен, хотя синтезируемые гипотезы при обычной ограниченности описания ПрО могут быть лишь правдоподобными, почему и нужна их оценка человеком. Известны системы логического вывода, похожим образом ориентированные на задачи синтеза гипотез, не противоречащих теории и «объясняющих наблюдаемое», например, в стиле задач диагностики «причина-эффект» в первопорядковой логике [30]. В них в роли свойства F выступает логическое следование наблюдаемого факта из базовой совокупности знаний (теории), а H‒ условие этого следования как объяснение наблюдаемого. При этом в разработках по абдуктивному выводу, помимо или вместо привлечения эксперта, часто используется некоторое множество потенциально возможных вариантов эмпирических гипотез, предполагаемое априори заданным на основе имеющегося прошлого опыта. Из альтернативно синтезированных тем или иным способом гипотез выбирается гипотеза, принадлежащая этому множеству.

В известных работах по выводу с абдукцией формульное представление знаний часто бывает ограничено требованием хорновости [31], типичным для логического программирования [32, 33]. Ограничением другого типа часто выступает требование, чтобы знания теории представлялись эквивалентностями в словаре переменных-причин и переменных-эффектов (с возможной частичной упорядоченностью эквивалентностей между собой импликациями). Таковыми в пропозициональном случае являются эквивалентности переменных-причин дизъюнкциям элементарных конъюнкций, составленных из переменных-эффектов и их отрицаний [30, 34].

Программные разработки на базе предложенного в работе метода интерактивного синтеза новых знаний с участием эксперта могут нуждаться в совершенствовании с учётом опыта использования, например, при реализации метода в составе некоторой экспертной или оперативно-советующей системы в медицине, авиации, учебном процессе и других приложениях [35-37]. Это, например, может быть связано с возможными ситуациями сомнения или несогласия конечного пользователя (оператора, врача, пилота, учителя и т.п.) с синтезированным объяснением или рекомендацией системы даже при её способности объяснять и наблюдаемое, и свои решения. Аккумулирование таких случаев и объяснений пользователя, обладающего системным, холистическим взглядом на ПрО, с верификацией оснований для сомнений пользователя может быть полезным для совершенствования системы.

В разделе 1 данной работы вводятся основные понятия и формулируется постановка рассматриваемой задачи. В разделе 2 вводится исчисление дедуктивно-абдуктивного типа J₊. Излагаются и обосновываются свойства его правил синтеза с точки зрения необходимости и достаточности синтезируемого. В разделе 3 приводятся примеры анализа свойств F описания ПрО и синтеза гипотез H как условий доказуемости F. В заключении формулируются итоги работы и задачи на будущее.

1  Основные понятия и постановка задачи

Язык пос-формул [10] построен на базе позитивных ТК, а именно: ТК всеобщности (ТКВ) $\forall X:W$ и ТК существования (ТКС) $\exists X:W$. Здесь X={x₁,…,x_k} ‒ множество предметных переменных $(k\ge 0)$, а W ‒ ти́повое условие, накладываемое как на эти переменные, так и, может быть, на переменные, связанные другими ТК, в область действия которых в пос-формуле входит рассматриваемый ТК. ТК именуется позитивным, если ти́повое условие ‒ конъюнкт, т.е. конъюнкция атомов или пропозициональная константа t либо f (true и false, соответственно). Далее рассматриваемые ТК считаются позитивными.

Определение 1 (пос-формулы). Пусть $Q\in \{\forall ,\exists \}$, а через $\overline{Q}$ обозначен символ $\exists$, если $Q=\forall ,$и символ $\forall ,$ если$Q=\exists$. Тогда:

1)  $QX:W$‒ $Q$-формула;

2) если $G_1\mathrm{,...,}{G}_n-Q$-формулы, то  $\overline{Q}X:W\left\{G_1\mathrm{,...,}{G}_n\right\}$‒ $\overline{Q}$-формула;

3) все $Q$-формулы являются поc-формулами; других поc-формул нет.

Отсутствие в синтаксисе поc-формул символа отрицания объясняет название формул. Язык L состоит из пос-формул. Подмножество языка  L, состоящее из $\exists$-формул, обозначается $L^{\exists }.$ Существенное отличие языка  L от других языков представления знаний состоит в сборке пос-формул только из ТК.

Семантика пос-формул F, $F\in L$, определяется [10] через семантику соответствующих им формул языка ИП. Представление пос-формулы F в языке ИП обозначается $F^{\text{'}}$. Соответствие задаётся следующим отображением:

1) $(\forall X:W\{G_1\mathrm{,...,}{G}_n\}{)}^{\text{'}}=\forall x_1\mathrm{...}\forall x_k(W\to {G_1}^{\text{'}}\vee \mathrm{...}\vee {G_n}^{\text{'}})$ (при этом$G_1\mathrm{,...,}{G}_n-$$\exists -$формулы);

2) $(\exists X:W\{G_1\mathrm{,...,}{G}_n\}{)}^{\text{'}}=\exists x_1\mathrm{...}\exists x_k(W\wedge {G_1}^{\text{'}}\wedge \mathrm{...}\wedge {G_n}^{\text{'}})$ (здесь$G_1\mathrm{,...,}{G}_n-$$\forall -$ формулы);

3) $(\forall X:W{)}^{\text{'}}=(\forall X:W\Phi {)}^{\text{'}}$, где  Ф‒ пусто, поэтому  $(\forall X:W{)}^{\text{'}}=(\forall X:W\Phi {)}^{\text{'}}\leftrightarrow$

$\leftrightarrow \forall x_1\mathrm{...}\forall x_k(W\to f)\leftrightarrow \forall x_1\mathrm{...}\forall x_k\neg W$ (дизъюнкция набора Ф формул $G_1\mathrm{,...,}{G}_n$, пустого при $n=0$, ложна);

4) $(\exists X:W{)}^{\text{'}}=(\exists X:W\Phi {)}^{\text{'}}\leftrightarrow \exists x_1\mathrm{...}\exists x_k(W\wedge t)\leftrightarrow \exists x_1\mathrm{...}\exists x_{k}W$ (конъюнкция пустого набора Ф пос-формул истинна).

Таким образом, структура пос-формулы может ветвиться дизъюнктивно после ТКВ и конъюнктивно после ТКС, а ТКВ и ТКС могут входить в ветвь пос-формулы только поочерёдно. Далее считается, что обозначения кванторных переменных двух ТК, один из которых входит в область действия другого, не пересекаются. Метод трансляции формул языка ИП в формулы языка L описан, например, в [18]. Язык L полон [10] относительно выразительной силы языка ИП.

Обычные понятия логической эквивалентности, следования и другие будут пониматься в языке L как в языке ИП, так как L можно считать собственным подмножеством множества формул языка ИП. Представление формулы  языка ИП в L обозначается ${\left(F\right)}^L$. Если в метаязыке выражение построено из пос-формул как подформул с помощью некоторых из логических символов $\to ,\leftrightarrow ,\neg ,\wedge ,\vee$, то вместо пос-формул следует понимать их образы в языке ИП. Так, если из контекста ясно, что $F_1,F_2\in L$, то запись $F_1\to F_2$ понимается как $(F_1{)}^{\text{'}}\to (F_2{)}^{\text{'}}$, т.е. как общезначимая, или истинная в любой интерпретации, формула, а в силу полноты ИП относительно выводимости это означает и выводимость в ИП.

Замечание 1. Язык позитивных формул [21, 38], как собственное подмножество языка ИП, не использует ТК и существенно у́же языка пос-формул и, тем более, пон-формул. Позитивные формулы в смысле [21, 38] используют только логические связки $\wedge$, $\vee$ и обычные кванторы, не используя отрицания и импликации. Позитивность пос-формул проявляется в двух смыслах: 1) структура допускает только $\wedge$- и $\vee$-ветвления; 2) структура собрана из ТК, ти́повые условия которых суть конъюнкты без отрицаний атомов [9]. При переводе пос- или пон-формул в язык ИП проявляются импликации ТКВ. Это обеспечивает полноту языка пос-формул относительно выразительности языка ИП и, в том числе, подмножества его формул с отрицаниями. Язык пон-формул: а) позитивен в первом смысле, б) может быть более высокого порядка, чем первый порядок, в) может быть частично формализованным и г) предложен для решения логических уравнений, имеющих структуру теорем о сохранении свойств связанных математических моделей.

Если при символе Q пос-формулы кванторные переменные отсутствуют (k=0), то символ Q не удаляется для конкретизации смысла связки $\to$ или $\wedge$, ассоциируемой с посылочным или утвердительным смыслом ти́пового условия W в ТКВ и ТКС соответственно. Если в пос-формуле кванторные переменные отсутствуют (при всех символах Q и во всех ти́повых условиях), то множество таких пос-формул может рассматриваться как подмножество пропозиционального языка, полное относительно выразительности пропозиционального языка.

Определение 2. Каноническим видом пос-формулы $V,V\in L,$  считается её представление с корневым ТКВ  $\forall :t$, т.е. в виде $V=\forall :t\Omega$, где $\Omega \subset L^{\exists }$ и $\Omega$ ‒ непустое множество $\exists$-формул, именуемых базовыми подформулами (БП).

В множестве  канонического представления формулы $V$ выделена одна подформула $G$ как образец преобразований всех $\exists$-формул из $\Omega =\{G,\Sigma \}$ по описываемому ниже правилу вывода $\omega$. Здесь $\Sigma$ ‒ подмножество прочих БП (возможно, пустое), строение которых аналогично следующему строению формулы G

$G=\exists X:A\Phi ,\Phi =\{\forall Y_1:B_1{\Psi }_1,\mathrm{...},\forall Y_n:B_n{\Psi }_n\},$$n\ge 0.$(1)

Каждый ТКС, как узел структуры пос-формулы, смежный корню $\forall :t$, является корневым для БП так же, как ТКС $\exists X:A$ для Ф. Он именуется базой (фактов), а его конъюнкт (в ТКС $\exists X:A$ это конъюнкт А) ‒ базовым конъюнктом. Узлы, дочерние базе, т.е. ТКВ (для ТКС $\exists X:A$ это ТКВ $\forall Y_{\text{}i}:B_i$), называются вопросами к базе, а подформулы, находящиеся в области действия базы (для ТКС $\exists X:A$ это подформулы  $\forall Y_{\text{}i}:B_i{\Psi }_i$), ‒ закономерностями базы (они у некоторых баз могут отсутствовать, когда $n=0).$ Пос-формулы, все БП которых не содержат ТКВ с ветвлением (т.е. ТКВ с дизъюнктивными ветвлениями), называются хорновскими, по аналогии с [31].

Отображение $\theta :\left(Y_i\right)\to X$ (частичное из множества Y_i в множество X) именуется подстановкой (контексты употребления символа  одновременно в теоретико-множественном и логическом смыслах исключают коллизии). Через $B_i\theta$ обозначается результат замены в B_i переменных из множества Y_i на некоторые переменные из X. Если $B_i\theta \subseteq A$, то $\theta$ отображение  называется ответной подстановкой, а вопрос $\forall Y_{\text{}i}:B_i$ ‒ уместным вопросом.

Определение 3 (правило вывода $\omega :L\to L$). Пусть пос-формула V отлична от $\perp$ и представлена в каноническом виде $V=\forall :t\Omega$, где $\Omega =\{G,\Sigma \}$, G имеет вид (1), но $n\ne 0,$т.е. в множество закономерностей Ф базы не пусто, и для некоторого $i\in \overline{\mathrm{1,}n}$$B_i\theta \subseteq A$, а ${\Psi }_i=\{\exists Z_{i1}:{С}_{i1}{\Psi }_{i1},\mathrm{...},\exists Z_{im}:{С}_{im}{\Psi }_{im}\}$. Тогда $\omega V=\text{\hspace{0.33em}\hspace{0.33em}}\forall :t\{{\Xi }_1\mathrm{,...,}{\Xi }_m,\Sigma \},\forall s\in \overline{\mathrm{1,}m}\text{\hspace{0.33em}\hspace{0.33em}\hspace{0.33em}}{\Xi }_s=\exists X\cup Z_{is}^{*}:A\cup {С}_{is}\theta (Z_{is}/Z_{is}^{*})$$\left\{{\Psi }_{is}\theta \right(Z_{is}/Z_{is}^{*}),\Phi \},$

где  $Z_{is}^{}/Z_{is}^{*}$‒ разыменование кванторных переменных, т.е. замена элементов множества $Z_{is}^{}$ на новые переменные из $Z_{is}^{*}$.

Правило $\omega :L\to L$ является логически эквивалентным преобразованием [10]. В яыке L пос-формул с применением этого правила введено исчисление $J=(\perp ,\omega )$ [9, 10], где формула $\perp =\forall :t\exists :f$ ‒ признак завершения вывода. Она является противоречием, поскольку в исчислении J доказательство всякой теоремы F ведётся от противного, как, например, и в [5]: опровергается отрицание V = (¬ F)^L доказываемого. Формула V из L называется выводимой в J (это записывается $\underset{J}{\vdash }V$ или $V\underset{J}{\vdash }\perp$), если $\exists s:s\ge 1{\omega }^{s}V=\perp$, т.е. на некотором шаге применения правила $\omega$ получается $\perp$. Исчисление J полно относительно выводимости [10]: отрицание всякой теоремы в ИП, представленное пос-формулой в языке L, выводимо в исчислении J. Наоборот, если пос-формула выводима в исчислении J, то отрицание её образа в языке ИП ‒ теорема ИП, т.е. общезначимо. Простейший пример невыводимой формулы возникает в случае, когда какая-то БП не содержит закономерностей ($n=0$). Необходимым условием опровержимости пос-формулы является наличие листового узла $\exists :f$ как потенциального «источника» проникновения в базу фактов атома f.

В случае наличия прикорневого ветвления структуры пос-формулы V, задача опровержения V ввиду дизъюнктивности ветвления сводится к независимым и аналогичным друг другу подзадачам опровержения своей БП. Проникновение в базовый конъюнкт константы f означает логическую эквивалентность базового конъюнкта и всей БП константе f; поэтому в случае единственности этой БП процесс опровержения завершён, а при неединственности она удаляется (это является логически эквивалентным преобразованием) с переходом к уместным вопросам других баз, и вывод по замыслу должен продолжаться до получения аналогичного эффекта во всех базах, если F была противоречивой.

Пусть F ‒ формула в языке ИП. Её дедуктивная проверка на доказуемость в исчислении $J=(\perp ,\omega )$ состоит в опровержении пос-формулы ${(\neg F)}^L$, т.е. в выводе ${(\neg F)}^L\underset{J}{├}\perp$ или $\text{\hspace{0.17em}├\hspace{0.17em}}F$ в ИП.

2  Синтез гипотез

Пусть $V\in L$ и в канонической форме $V=\forall :t\{G,\Sigma \}$, где  G‒ выделенная БП вида (1), а  $\Sigma$‒ множество прочих БП.

В исчислении $J_{+}=(\perp ,\omega ,\delta )$ вводится первый тип правил $\delta$. Это определяемые ниже правила $\alpha$ первичного преобразования пос-формул. Им будут соответствовать гипотезы H первичного типа. Правила  расширяют множество закономерностей некоторой базы обрабатываемой пос-формулы гипотезой H, корневой узел которой является заведомо уместным вопросом. Поэтому в ситуации непродолжимости вывода в исчислении $J=(\perp ,\omega )$, т.е. неприменимости правила $\omega$, применение правила $\alpha$ заведомо продолжает вывод.

Определение 4 (правила $\alpha$ первичного преобразования пос-формул). Правила $\alpha$‒ это преобразования $\alpha :L\to L,\alpha \left(V\right)=V(\Phi /\{\Phi ,H\left\}\right)$, где H. ‒ поc-формула, предполагаемая замкнутой (не содержащей свободных вхождений кванторных переменных), а преобразование $\alpha$ в зависимости от H имеет вид:

а) $\alpha ={\alpha }_0$, когда $H=H_0=\forall X^{*}:A\exists :f$ (при $n=0$);                                             (2)

б) $\alpha ={\alpha }_{\vee }$, когда $H=H_{\vee }=\forall X^{*}:A\{\exists Y_1^{*}:B_1\mathrm{,...,}\exists Y_n^{*}:B_n\}$(при $n>1$ );            (3)

в) $\forall i\in \overline{\mathrm{1,}n}\alpha ={\alpha }_i,$ когда $H=H_i=\forall X^{*}:A\exists Y_i^{*}:B_i$ (при $n\ge 1$).                          (4)

Здесь верхний индекс $*$ означает разыменование в H кванторных переменных (для исключения их совпадения с переменными, входящими в корень $\exists X:A$ и его дочерние узлы $\forall Y_i:B_i(i\in \overline{\mathrm{1,}n)}$ из G). При позитивности конъюнктов $A,A_i,B_i$, вытекающей из определения пос-формул, гипотезы H непротиворечивы. Логические связи свойства F и гипотез H представлены в следующей теореме.

Теорема 1 (о связи свойства F и гипотез H первичного типа). Пусть F ‒ изучаемое свойство описания ПрО, а H ‒ гипотеза первичного типа, $F={(\neg F)}^L,S={\omega }^{s_2}\alpha {\omega }^{s_1}F$, где  $s_i\ge 0$ $(i\in \overline{\mathrm{1,2}}).$ Тогда $\underset{J}{\overset{}{├}}T$, где $T=\neg (\neg S\wedge H\to F)$, т.е. $\neg S\wedge H\to F$. В частности:

1) если $S=\perp$, то  $H\to F$(условие H достаточно для F);

2) если $\alpha \in \{{\alpha }_0,{\alpha }_{\vee }\}$, то  $F\to H$  (условия $H_0$ и $H_{\vee }$ необходимы для F).

Доказательство. Необходимо показать достаточность условия$\neg S\wedge H$ для F при любом $\alpha \in \{{\alpha }_0,{\alpha }_{\vee },{\alpha }_i\}$. Пусть синтез гипотезы H выполнен применением правила $\alpha$ к пос-формуле V, полученной из F $s_1$-кратным применением правила $\omega$, т.е. к формуле $V={\omega }^{s_1}F=\forall :t\{G,\Sigma \}$, где $G=\exists X:A\Phi$ и $\Phi =\{\forall Y_1:B_1{\Xi }_1\mathrm{,...,}\forall Y_n:B_n{\Xi }_n\}$. Тогда

  $S={\omega }^{s_2}\alpha \left(V\right)\leftrightarrow \alpha \left(V\right)=$$V(G/(G(\Phi /\{\Phi ,H\left\}\right)\left)\right)$$=\forall :t\left\{G\right(\Phi /\{\Phi ,H\}),\Sigma \}$,

а так как $H=H\left(X^{*}\right)$ и не содержит вхождений переменной X, то

    $G(\Phi /\{\Phi ,H\left\}\right)\leftrightarrow \exists X(A^{\text{'}}\wedge {\Phi }^{\text{'}}\wedge H^{\text{'}})\leftrightarrow G^{\text{'}}\wedge H^{\text{'}}$                              

и поэтому $S\leftrightarrow (G\wedge H)\vee \Sigma$. Это значит, что $\neg S\to \neg \left(\right(G\wedge H)\vee \Sigma )\leftrightarrow$$(H\to \neg G)\wedge \neg \Sigma$. Отсюда следует $\neg S\wedge H\to \neg G\wedge \neg \Sigma \leftrightarrow \neg V\leftrightarrow \neg F=F$. С учётом этого и того, что при $S=\perp$ справедливо $\neg S\wedge H\leftrightarrow H$, получается утверждение 1) доказываемой теоремы.

Пусть теперь $\alpha \in \{{\alpha }_0,{\alpha }_{\vee }\}$. Требуется показать необходимость соответствующих гипотез первичного типа $H_0$ и $H_{\vee }$ (см. (2) и (3)). Если $\alpha ={\alpha }_0$, то $\neg F\leftrightarrow \neg V\leftrightarrow \neg G\wedge \neg \Sigma =\forall X:A\exists :f\wedge \neg \Sigma$, откуда очевидным образом следует $H_0$.

Если же $\alpha ={\alpha }_{\vee }$, то $\neg F\leftrightarrow \neg V\leftrightarrow \neg G\wedge \neg \Sigma =$$\forall X:A\{\exists Y_1:B_1\neg {\Xi }_1\mathrm{,...,}\exists Y_n:B_n\neg {\Xi }_n\}\wedge \neg \Sigma$.

Из сравнения этого с условием $H_{\vee }$ видно, что $\neg F\to H_{\vee }$. Теорема доказана.

Замечание 2. По определению (2) правила ${\alpha }_0$ при $n=0$, т.е. при пустом множестве Ф, формировалась гипотеза $H=H_0=\forall X^{*}:A\exists :f$ как условие противоречивости базового конъюнкта А. Подразумевается, что эта гипотеза без дальнейших преобразований включается в конъюнктивный набор гипотез, синтезированных по всем БП из $\Omega =\{G,\Sigma \}$, с отслеживанием непоявления гипотезы, обуславливающей $\exists X:A$ и потому противоречащей $H_0$. Далее в БП $n\ge 1$.

Замечание 3. При $n>1$ согласно (3) структура гипотезы $H_{\vee }$ нехорновская, т.е. содержит $\vee$-ветвление: $H_{\vee }=\forall X^{*}:A\{\exists Y_1^{*}:B_1\mathrm{,...,}\exists Y_n^{*}:B_n\}$. Эксперту предлагается возможность корректировки и выбора $n+1$ вариантов гипотезы из множества $\left\{H_{\vee }\right\}\cup {\left\{H_i^{}\right\}}_{i\in \overline{\mathrm{1,}n}}$, где $\forall i\in \overline{\mathrm{1,}n}{H}_i^{}=\forall X^{*}:A\exists Y_i^{*}:B_i$. В общем случае эксперт может рассматривать и варианты, получаемые из $H_{\vee }$ удалением меньшего количества дизъюнктивно связанных ветвей, чем $n-1$. Ниже рассматриваются гипотезы H_i вида (4), как более «естественные» для теорем $H\to F$, чем нехорновская гипотеза $H_{\vee }$. В частности, при $Y_i^{*}=\varnothing$ гипотезы H_i имеют вид $(H_i^{}{)}^{\text{'}}=\forall X(A\left(X\right)\to B_i\left(X\right))$, т.е. простых условий типа «если …, то …», не только без $\vee$-ветвления, но и без квантора существования. Использование гипотез (4) предпочтительнее, чем вида (3), тем более при использовании правил в задачах с конструктивной семантикой [10, 36]. Финальный вид гипотез $H_i^{}$достигается применением в исчислении $J_{+}=(\perp ,\omega ,\delta )$ правил $\delta$ второго типа. Это правила $\beta$ преобразования $\forall$-формул $H_i^{}$, именуемые правилами вторичного преобразования пос-формул, как частичные отображения $\beta :\left(L^{\forall }\right)\to L,\beta \left(H_i\right)=H_i^{*}.$ Пос-формулы $H_i^{*}$ называются гипотезами вторичного типа.

Определение 5 (операции вторичного преобразования β пос-формул). Для всякого H_i вида  (4) преобразование β(H_i) состоит в некоторой суперпозиции определяемых ниже  операций ${\left\{O_i\right\}}_{i\in \overline{\mathrm{1,5}}}$, $O_i:\left(L^{\forall }\right)\to L$. Если  $V=\forall Z^1:C\exists Z^2:D$‒ формула H_i или общее обозначение результата применения предыдущих операций внутри преобразования β, то операциями преобразования  являются:

1) операция O₁ удаления некоторых атомов корневого конъюнкта C;

2) операция O₂ удаления из листового конъюнкта D повторов, т.е. атомов, возможно, вошедших в корневой конъюнкт C на предыдущих операциях;

3) операция O₃ подстановки $\theta :\left(Z^2\right)\to Z^1$;

4) операция O₄ удаления из множества Z¹ кванторных переменных корневого узла $\forall Z^1:C$ всех независимых переменных, т.е. не входящих $\forall :C\exists Z^2:D$;                                                                                                                                                              

5) если конъюнкты $C,D$ формулы $V=\forall Z^1:C\exists Z^2:D$ имеют вид $C=C_1\left(Z_1^1\right)\cup C_2\left(Z_2^1\right)$ и $D\left(Z_1^1\right)$, где $Z^1=Z_1^1\cup Z_2^1,Z_1^1\cap Z_2^1=\varnothing ,$ т.е. атомы C₁ и D не содержат переменных из $Z_2^1$, а $C_2$ не содержит переменных из $Z_1^1$, то $O_5\left(V\right)=V_1\wedge V_2$, $V_1=\forall Z_1^1:C_1\exists Z^2:D$,$V_2=\exists Z_2^1:C_2.$

Используемый далее для краткости термин «преобразование ПДУ» понимается как преобразование Перехода к Достаточному Условию. Т.е, если формула U₁  получена из U₂ преобразованием, обеспечивающим логическую импликацию $U_1\to U_2$, то это преобразование именуется как преобразование «перехода от U₂ к достаточному условию U₁». При этом U₁ не слабее, чем U₂, так как всякая логическая импликация включает и случай эквивалентности. В частности, для всякой формулы  $V,V\in L,$ ${\alpha }_i\left(V\right)$ логически не слабее, чем ${\alpha }_{\vee }\left(V\right)$.

Теорема 2 (о связи свойства F и гипотез $H_i^{*}$ вторичного типа). Если к гипотезе $H_i^{}$ вида (4) применено преобразование $\beta :\left(L^{\forall }\right)\to L,\beta \left(H_i\right)=H_i^{*}$, в виде той или иной суперпозиции некоторых операций $O_i$ из множества ${\left\{O_i\right\}}_{i\in \overline{\mathrm{1,5}}}$, $O_i:\left(L^{\forall }\right)\to L$, то ${(\neg (\beta \left(H_i\right)\to F\left)\right)}^L\underset{J}{}\perp$, т.е. синтезированный текст  $H_i^{*}\to F$‒ теорема.

Доказательство. Требуется проверить, что каждая из операций $O_i\in {\left\{O_i\right\}}_{i\in \overline{\mathrm{1,5}}}$ преобразования β сопровождается ПДУ. Пусть  $V=\forall Z^1:C^1\exists Z^2:D$‒ гипотеза$H_i^{}$ или результат предыдущих операций внутри преобразования β.

Применение операции O₁ удаления из C¹ некоторых атомов не сужает заданной типовым условием C¹ области значений кванторных переменных множества Z¹, и $O_1\left(V\right)$ не слабее, чем V, что означает ПДУ. Операция O₂ удаления повторов из конъюнкта D атомов, входящих в посылку C является логически эквивалентным преобразованием. Операция O₃ подстановки в  D вместо вхождений переменных множества  Z² соответствующих переменных из  Z¹‒ это снова ПДУ для V.

В связи с операциями O₄ и O₅ преобразования β следует отметить, что удаления независимых кванторов ‒ ти́повых и обычных ‒ различаются по результату. Например, пусть имеются две формулы $U_1=\forall xA\left]x\right[,$$U_2=\forall x\left(W\right(x)\to A]x\left[\right)$  , где $A\left]x\right[$ обозначает отсутствие в формуле A свободных вхождений переменной $x$, отчего обычный квантор $\forall x$ и ТКВ $\forall x:W\left(x\right)$ именуются независимыми. После их удаления из U₁ и U₂ результат A соотносится с формулами U₁ и U₂ по разному: $A\to U_1\wedge U_2$, $U_1\to A$, но U₂ влечёт A лишь при дополнительном условии $\exists xW\left(x\right)$, т.е. $\exists xW\left(x\right)\to (U_2\to A)$.

В силу сказанного, операция O₅, в отличие от операции O₄, не является логически эквивалентным преобразованием. Так как $O_5\left(V\right)=\exists Z_2^1{C}_2\wedge \forall Z_1^1(C_1\to \exists Z^{2}D)$ и $V=\forall Z^1:C\exists Z^2:D=\forall Z_1^1\cup Z_2^1:C_1\left(Z_1^1\right)\cup C_2\left(Z_2^1\right)\exists Z^2:D\leftrightarrow \forall Z_2^1(C_2\to \forall Z_1^1(C_1\to \exists Z^{2}D\left)\right),$

то $O_5\left(V\right)\to V$ и поэтому обеспечивается ПДУ. При этом удаляется независимый ТКВ $\forall Z_2^1:C_2$, что и потребовало конъюнктивного включения в гипотезу $O_5\left(V\right)$ условия $\exists Z_2^1{C}_2$.

Таким образом, все операции ${\left\{O_i\right\}}_{i\in \overline{\mathrm{1,5}}}$ преобразования β сопровождаются переходами к достаточным условиям и поэтому $(H_i^{*}{)}^{\text{'}}\to F$, где $H_i^{*}=\beta \left(H_i\right)$, т.е. ${(\neg ((H_i^{*}{)}^{\text{'}}\to F))}^L\underset{J}{}\perp$, что и требовалось доказать.

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

3  Примеры

Пусть предметом интереса человека является доступность самолётам высот тропосферы, как нижнего слоя атмосферы Земли, и стратосферы, как соседнего, более удалённого от планеты слоя. Предположим, что у человека-эксперта имеется предварительное описание предмета в форме некоторой совокупности V утверждений-знаний, возможно из разных источников этой ПрО. Описание является заготовкой к началу работы эксперта по интерактивному анализу этого описания с точки зрения свойств непротиворечивости, избыточности и других. Предполагается, что работа эксперта ведётся с применением исчисления $J_{+}=(\perp ,\omega ,\delta )$ для АД свойств и порождения новых знаний.

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

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

Для логической формализации этого описания задействуются следующие предикаты:

    $P\left(x\right)\iff «x-самолет»,$

    $T\left(y\right)\iff «y-высотавтропосфере»,$

    $S\left(y\right)\iff «y-высотавстратосфере»,$

     $R(x,y)\iff «дляxдоступноy»,$

     $L(y,z)\iff «z-ниже,чемy»$

(здесь $\iff$ означает «…тогда и только тогда, когда… », а обозначения предикатов ‒ от английских слов «Plane», «Troposphere», «Stratosphere», «Reachable», «Lower than»). В языке ИП (первого порядка) данное описание предмета рассмотрения примет вид

  $V=\exists x\exists y\left(P\right(x)\wedge S(y)\wedge R(x,y\left)\right)\wedge$

$\wedge \forall x\forall y\left(P\right(x)\wedge R(x,y)\to (\forall z\left(L\right(y,z)\to R(x,z\left)\right)\wedge$

    $\wedge \exists x\left(P\right(x\left)\right((\forall y(T\left(y\right)\to R(x,y))\wedge \exists y(S\left(y\right)\wedge R(x,y)\left)\right),$

что в переводе на язык  L пос-формул может быть записано в следующей канонической форме (с двумя -ветвлениями и тремя БП как базовыми закономерностями):           

        $V^L=\forall :t\exists :t$ $\left\{\begin{array}{l}\forall :t\exists x,y:P\left(x\right),\\ \\ \forall x_1,y_1:P\left(x_1\right),\\ \forall :t\exists x_2:P\left(x_2\right)\end{array}\right.$$\begin{array}{l}S\left(y\right),R(x,y)\\ \\ R(x_1,y_1)\\ \end{array}$

Для уменьшения потребности в разыменованиях кванторных переменных при применении правила $\omega$ (см. в разделе 1) необходимо исключать совпадение кванторных переменных не только в тех случаях, когда один ТК находится в области действия другого, но и в случаях, когда кванторные переменные входят в разные ветви. Поэтому далее используется представление с разыменованными кванторными переменными:

    $V^L=\forall :t\exists :t$ $\left\{\begin{array}{l}\forall :t\exists x,y:P\left(x\right),\\ \\ \forall x_1,y_1:P\left(x_1\right),\\ \forall :t\exists x_2:P\left(x_2\right)\end{array}\right.$ $\begin{array}{l}S\left(y\right),R(x,y)\\ \\ R(x_1,y_1)\\ \end{array}$                                                                                                                                                                              (5)

Пусть $V^L=\forall :t\exists :t \{V_1,V_2,V_3\}$  при следующих обозначениях для закономерностей:

 $V_1=\forall :t\exists x,y:P\left(x\right),S\left(y\right),R(x,y),$

$V_2=\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2),$            (6)

$V^L=\forall :t\exists x_2:P\left(x_2\right)\begin{array}{}\end{array}$ $\left\{\begin{array}{l}\forall y_3:T\left(y_3\right)\exists :R(x_2,y_3)\\ \forall :t\exists y_4:S\left(y_4\right),R(x_2,y_4).\end{array}\right.$

Здесь и далее БП нумеруются сверху вниз (как далее и при нумерации корневых узлов из БП, т.е. вопросов).

Утверждение (5) непротиворечиво, и это свойство в общем случае устанавливается автоматически в пос-исчислении $J$ путём проверки того, что вывод ${\left(V\right)}^L├\underset{J}{\overset{}{}}\perp$ не осуществим, т.е. формула ${\left(V\right)}^L$ не опровержима. Действительно, через три шага применения правила $\omega$ с пустыми ответными подстановками получается следующее:

$\begin{array}{cc}\begin{array}{l}{\omega }^3\left(V^L\right)=\forall :t\exists x,y,x_2,y_4:P\left(x\right),\\ S\left(y\right),R(x,y),\\ P\left(x_2\right),S\left(y_4\right),R(x_2,y_4)\end{array}& \left\{\begin{array}{l}\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \forall y_3:T\left(y_3\right)\exists :R(x_2,y_3).\end{array}\right.\end{array}$

                                         $\begin{array}{l}\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \end{array}$    

Теперь только первый вопрос  $\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)$- уместный. Ответная подстановка ${\theta }_1:x_1\to x,y_1\to y$ приводит к формул  

$\begin{array}{cc}\begin{array}{l}{\omega }^4\left(V^L\right)=\forall :t\exists x,y,x_2,y_4:P\left(x\right),\\ S\left(y\right),R(x,y),\\ P\left(x_2\right),S\left(y_4\right),R(x_2,y_4)\end{array}& \left\{\begin{array}{l}\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \forall y_3:T\left(y_3\right)\exists :R(x_2,y_3)\\ \forall y_5:L(y,y_5)\exists :R(x,y_5).\end{array}\right.\end{array}$                                            

После второго ответа на тот же вопрос с подстановкой ${\theta }_2:x_1\to x_2^{},y_1\to y_4$получается

$\begin{array}{cc}\begin{array}{l}{\omega }^5\left(V^L\right)=\forall :t\exists x,y,x_2,y_4:P\left(x\right),\\ S\left(y\right),R(x,y),\\ P\left(x_2\right),S\left(y_4\right),R(x_2,y_4)\end{array}& \left\{\begin{array}{l}\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \forall y_3:T\left(y_3\right)\exists :R(x_2,y_3)\\ \forall y_5:L(y,y_5)\exists :R(x,y_5)\\ \forall y_6:L(y_4,y_6)\exists :R(x_2,y_6).\end{array}\right.\end{array}$

          

Теперь первый вопрос больше неуместен, так как новых ответных подстановок в его конъюнкт нет. Остальные три вопроса тоже неуместны, поэтому вывод оказался в тупике непродолжимости, означающей, что в исчислении $J$ не выводимо $\perp$, т.е. формула $V$ непротиворечива.

Следует заметить, что приведённое рассуждение ‒ лишь иллюстрация применения правила $\omega$ в исчислении $J$; в действительности в этом частном случае исходной формулы $V^L$ вида (5) непротиворечивость усматривается сразу, а именно по факту отсутствия в $V^L$ ни одного листового узла в виде ТКС $\exists :f$. Стоит заметить, что этот признак не является достаточным: поc-формула может содержать ТКС $\exists :f$, но не быть противоречивой и поэтому в таких случаях проверка невыводимости $\perp$ является обязательной как проверка попадания в ситуацию непродолжимости вывода, что и сделано выше.

Пример 2 (проверка следования одних утверждений из других, синтез условия следования). Например, для каждого утверждения $V_i$ из ${\left(V\right)}^L$(см. (6)) может делаться проверка его логического следования из остальных. Если такое следование имеет место, то может выявляться минимальный набор утверждений, из которых следует рассматриваемое утверждение. Таких наборов может быть несколько. Результаты такой проверки на избыточность сообщаются эксперту.

Описание ${\left(V\right)}^L$ предмета рассмотрения избыточно, так как $V_i$ следует из минимального одноэлементного набора {$V_3$}. Эксперт может удалить $V_i$ или исключить из $V_3$ подформулу $\forall :t\exists y_4:S\left(y_4\right),R(x_2,y_4)$. Эксперт, видя, что $V_3$ не следует из $V_1\wedge V_2$, может заинтересоваться, например, синтезом условия H, достаточного для $V_1\wedge V_2\to V_3$, с тем, чтобы, если условие H будет лаконичнее, чем $V_3$, то заменить $V_3$ на H.

Проверка свойства $F=V_1\wedge V_2\to V_3$ осуществляется автоматически как проверка выводимости $\perp$ из $F=\neg F={(V_1\wedge V_2\wedge \neg V_3)}^L$ в исчислении $J=(\omega ,\perp )$. Формула F в языке L представима с одной БП $\Omega$:

 $\begin{array}{cc}F=\forall :t\exists :t\Omega =\forall :t\exists :t& \left\{\begin{array}{l}\forall :t\exists x,y:P\left(x\right),S\left(y\right),R(x,y)\\ \\ \forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \begin{array}{cc}\forall x_2:P\left(x_2\right)& \left\{\begin{array}{l}\exists y_3:T\left(y_3\right)\forall :R(x_2,y_3)\exists :f\\ \exists :t\forall y_4:S\left(y_4\right),R(x_2,y_4)\exists :f.\end{array}\right.\end{array}\end{array}\right.\end{array}$(7)

Так как третья закономерность в (7) имеет $\vee$-ветвление, то она нехорновского типа, и поэтому в дальнейшем БП расщепится на две БП. Пока же после ответа на тривиальный вопрос из $V_1$ (с пустой подстановкой $\theta$) получится

$\begin{array}{cc}F=\forall :t\exists :t\Omega =\forall :t\exists :t& \left\{\begin{array}{l}\forall :t\exists x,y:P\left(x\right),S\left(y\right),R(x,y)\\ \\ \forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \begin{array}{cc}\forall x_2:P\left(x_2\right)& \left\{\begin{array}{l}\exists y_3:T\left(y_3\right)\forall :R(x_2,y_3)\exists :f\\ \exists :t\forall y_4:S\left(y_4\right),R(x_2,y_4)\exists :f.\end{array}\right.\end{array}\end{array}\right.\end{array}$(8)

Теперь возможны ответы на оба вопроса.

При ответе на первый с ответной подстановкой ${\theta }_3:x_1\to x,y_1\to y$ получается

$\begin{array}{cc}\begin{array}{l}{\omega }^2\left(F\right)=\forall :t\exists x,y:P\left(x\right),S\left(y\right),\\ R(x,y)\end{array}& \left\{\begin{array}{l}\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \forall x_2:P\left(x_2\right)\left\{\begin{array}{l}\exists y_3:T\left(y_3\right)\forall :R(x_2,y_3)\exists :f\\ \exists :t\forall y_4:S\left(y_4\right),R(x_2,y_4)\exists :f\end{array}\right.\\ \forall y_2:L(y,y_2)\exists :R(x,y_2).\end{array}\right.\end{array}$

При ответе на вопрос $\forall x_2:P\left(x_2\right)$ с ответной подстановкой ${\theta }_4:x_2\to x$ БП из ${\omega }^2\left(F\right)$ расщепится: $\omega {}^3\left(F\right)=\forall :t\{{\Omega }_1,{\Omega }_2\}$, где

${\Omega }_1=\exists x,y,y_5:P\left(x\right),S\left(y\right),R(x,y),T\left(y_5\right)$     $\left\{\begin{array}{l}\Sigma \\ \begin{array}{cc}\forall :R(x,y_5)\exists :f,& \end{array}\end{array}\right.$ (9)

${\Omega }_2=\exists x,y:P\left(x\right),S\left(y\right),R(x,y)$   $\left\{\begin{array}{l}\Sigma \\ \begin{array}{cc}\forall y_5:S\left(y_5\right),R(x,y_5)\exists :f,& \end{array}\end{array}\right.$

 $\begin{array}{cc}\Sigma =& \begin{array}{l}\left\{\begin{array}{l}\forall x_1,y_1:P\left(x_1\right),R(x_1,y_1)\exists :t\forall y_2:L(y_1,y_2)\exists :R(x_1,y_2)\\ \forall x_2:P\left(x_2\right)\left\{\begin{array}{l}\exists y_3:T\left(y_3\right)\forall :R(x_2,y_3)\exists :f\\ \exists :t\forall y_4:S\left(y_4\right),R(x_2,y_4)\exists :f\end{array}\right.\\ \forall y_2:L(y,y_2)\exists :R(x,y_2).\end{array}\right.\\ \end{array}\end{array}$    (10)

В отличие от первой подзадачи, вторая (опровержения ${\Omega }_2$) разрешается положительно за один шаг применения $\omega$ с ответной подстановкой ${\theta }_5:y_5\to y$, приводя к $\perp$, что не достигается в первой подзадаче (опровержения ${\Omega }_1$). Действительно, вопрос $\forall x_2:P\left(x_2\right)$ перестал быть уместным, так как, несмотря на пополнение базы атомом $T\left(y_5\right)$, ответной подстановки, отличной от уже использованной ${\theta }_4:x_2\to x$, не появилось. Поэтому в исчислении $J=(\perp ,\omega )$ БП ${\Omega }_1$, а значит и в целом F неопровержимы, так как $F\leftrightarrow \omega {}^3{\left(F\right)}^L=\forall :t\{{\Omega }_1,{\Omega }_2\}$. Таким образом, F, как отрицание импликации $V_1\wedge V_2\to V_3$, неопровержимо и $V_3$ не следует из $V_1\wedge V_2.$ При другом порядке ответа на вопросы из (8) результат обязан быть тем же.

Эксперта может интересовать, какого условия H не хватает для $V_1\wedge V_2\to V_3$ с тем, чтобы при лаконичности этого H заменить им «громоздкое» V₃. В продолжение примера 1 для синтеза этого H применяется исчисление $J_{+}=(\perp ,\omega ,\delta )$, $\delta \in \{\alpha ,\beta \},\alpha \in \{{\alpha }_0,{\alpha }_{\vee },{\alpha }_i\},\beta \in {\left\{{\beta }_j\right\}}_{j\in \overline{\mathrm{1,6}}}$. При выборе  $\delta ={\alpha }_{\vee }$

$H_{\vee }=\forall x^{*},y^{*},y_5^{*}:P\left(x^{*}\right),S\left(y^{*}\right),R(x^{*},y^{*}),T\left(y_5^{*}\right)$      $\left\{\begin{array}{l}\exists x_1^{*},y_1^{*}:P\left(x_1^{*}\right),R(x_1^{*},y_1^{*})\\ \begin{array}{cc}\begin{array}{l}\exists x_2^{*}:P\left(x_2^{*}\right)\\ \exists y_2^{*}:L(y^{*},y_2^{*})\\ \exists :R(x^{*},y_5^{*})\end{array}& \end{array}\end{array}\right.$                                                                                                              (11)

${\alpha }_{\vee }{\Omega }_1=\exists x,y,y_5:P\left(x\right),S\left(y\right),R(x,y),T\left(y_5\right)\{\Sigma ,(\forall :R(x,y_5)\exists :f),H_{\vee }\}.$

В $\exists$-формуле ${\Omega }_1$ вида (9-10) содержатся четыре закономерности, из которых две последние кажутся перспективными для опровержения ${\Omega }_1$. Это

  $\forall y_2:L(y,y_2)\exists :R(x,y_2)$, $\forall :R(x,y_5)\exists :f$,                                           (12)

активизируемые на основе начальных гипотез H₃ и H₄ по правилам ${\alpha }_i.$

Согласно гипотезе первичного типа H₃:

  $H_3=\forall x^{*},y^{*},y_5^{*}:P\left(x^{*}\right),S\left(y^{*}\right),R(x^{*},y^{*}),T\left(y_5^{*}\right)\exists y_2^{*}:L(y^{*},y_2^{*})$.       (13)

Действительно, в применении к (9) гипотеза H₃ может позволить нарастить базу в ${\Omega }_1$ атомом $L(\cdot ,\cdot )$, задействуя вначале третью закономерность из (10), а далее, после попадания в базу атома $R(x,y_5)$, и четвёртую закономерность из (9) с опровержением ${\Omega }_1$. Это будет означать опровержимость и в целом сделанного предположения $F={(V_1\wedge V_2\wedge \neg V_3)}^L$, которое логически эквивалентно $\omega {}^2{\left(F\right)}^L=\forall :t\{{\Omega }_1,{\Omega }_2\}$. Можно проверить реализуемость синтеза требуемого условия для замещения $V_3$. По правилу ${\alpha }_3$ формируется расширение закономерностей в БП ${\Omega }_1$ гипотезой (13):

             ${\alpha }_3{\Omega }_1=\exists x,y,y_5:P\left(x\right),S\left(y\right),R(x,y),T\left(y_5\right)\{\Sigma ,(\forall :R(x,y_5)\exists :f),H_3\}$ .

После подстановки ${\theta }_6:y_2^{*}\to y_5^{*}$ в (13) получается утверждение

              $O_3\left(H_3\right)=\forall x^{*},y^{*},y_5^{*}:P\left(x^{*}\right),S\left(y^{*}\right),R(x^{*},y^{*}),T\left(y_5^{*}\right)\exists :L(y^{*},y_5^{*})$,

означающее: «Для любой стратосферной высоты и любого самолёта, которому эта высота доступна, любая тропосферная высота ‒ ниже ». С позиции упрощения гипотезы эксперт заметит нецелесообразную ограничительность посылки и применит операцию $O_1$ удаления атомов $P\left(x^{*}\right),R(x^{*},y^{*})$. После этого квантор $\forall x^{*}$становится независимым и удаляется согласно $O_4$. Получится гипотеза

  $O_4{O}_1{O}_3\left(H_3\right)=\forall y^{*},y_5^{*}:S\left(y^{*}\right),T\left(y_5^{*}\right)\exists :L(y^{*},y_5^{*})$,                        (14)

означающая, что «Тропосферные высоты ниже стратосферных» .

После подстановки ${\theta }_7:y^{*}\to y,y_5^{*}\to y_5$ база в (9) дополнится атомом $L(y,y_5^{})$, приведя к уместности третьего вопроса в (9). Ответная подстановка ${\theta }_8:y_2\to y_5$ обеспечит попадание в базу из (9) атома $R(x,y_5)$ и уместность вопроса четвёртой закономерности из (9). Ответ на него с пустой подстановкой приведёт к проникновению в базу из (9) константы f, т.е. к опровержению БП ${\Omega }_1$.

По теоремам 1 и 2 гипотеза (вторичного типа) $H_3^{*}$ вида (14) является достаточным условием доказуемости свойства $F=V_1\wedge V_2\to V_3$. Поэтому в описании предмета рассмотрения (см. ${\left(V\right)}^L$ вида (6)) утверждение $V_3$ можно заменить на (14).

Пример 3 (синтез гипотезы, альтернативной гипотезе (14)). Из ранее выделенных в (12) двух закономерностей для синтеза гипотезы, достаточной для $V_1\wedge V_2\to V_3$, можно выбрать четвёртую закономерность, для задействования которой в множестве усилений (точнее логических неослаблений) условия (11), получаемых разделением ветвей, по правилу ${\alpha }_4$ выбрать гипотезу

$H_4=$ $\forall x^{*},y^{*},y_5^{*}:P\left(x^{*}\right),S\left(y^{*}\right),R(x^{*},y^{*}),T\left(y_5^{*}\right)\exists :R(x^{*},y_5^{*}).$         (15)

Получится

${\alpha }_4{\Omega }_1=\left({\alpha }_{\vee }{\Omega }_1\right)(H_{\vee }/H_4)=\exists x,y,y_5:$$P\left(x\right),S\left(y\right),R(x,y),T\left(y_5\right)\{\Sigma ,(\forall :R(x,y_5)\exists :f),H_4\}.$

Ответная подстановка ${\theta }_9:x^{*}\to x,y_5^{*}\to y_5$ с применением правила $\omega$ дополнит базу из ${\Omega }_1$ атомом $R(x,y_5)$ и с учётом закономерности $\forall :R(x,y_5)\exists :f$ из ${\Omega }_1$ (см. (9)) приводит к желаемому опровержению БП ${\Omega }_1$, причём более коротким путём, чем в примере 2. Гипотеза первичного типа H₄ в форме (15) означает: «Для любого самолёта и любой доступной ему стратосферной высоты любая тропосферная высота тоже доступна», или, что эквивалентно: «Для любой стратосферной высоты и любого самолёта, которому эта высота доступна, любая тропосферная высота тоже доступна».

Из операций преобразования $\beta$ применима только операция $O_1$. Если эксперт операцией $O_1$ удалит атомы $S\left(y^{*}\right),R(x^{*},y^{*})$, то потом операцией $O_4$ удалится и квантор $\forall y^{*}$, становящийся независимым. Это приведёт к семантически более простой гипотезе вторичного типа

  $O_4{O}_1\left(H_4\right)=\forall x^{*},y_5^{*}:P\left(x^{*}\right),T\left(y_5^{*}\right)\exists :R(x^{*},y_5^{*})$,                             (16)

означающей: «Самолётам все тропосферные высоты доступны».

Гипотеза (16) является примером гипотезы логически верной с точки зрения её достаточности для доказуемости свойства $V_1\wedge V_2\to V_3$, но неверной при учёте знаний, не охваченных описанием предмета (V)^L. Это так, поскольку разнообразие самолётов в описании (V)^L не ограничено и, в частности, включает модели низковысотные, которым верхние высоты тропосферы недоступны. Эксперту придётся задуматься над содержанием используемого им понятия «Самолёт» и при определённой широте этого понятия отказаться от замещения утверждения $V_3$ в описании (V)^L ПрО (см. (6)) условием (16) и вместо этого использовать ранее синтезированную гипотезу (14)

              $H_3^{*}=O_4{O}_1{O}_3\left(H_3\right)=\forall y^{*},y_5^{*}:S\left(y^{*}\right),T\left(y_5^{*}\right)\exists :L(y^{*},y_5^{*})$,

согласно которой «Тропосферные высоты ниже стратосферных».

Заключение

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

Предложенный метод синтеза новых знаний объединяет возможности анализа знаний на основе АД с алгоритмизированным человеко-машинным формированием текстов утверждений. При автоматическом выявлении в описании ПрО отсутствия свойства, желательного для человека, задействуется расширение исчисления дополнительными правилами, которые обеспечивают синтез условия-гипотезы, логически гарантирующей наличие требуемого свойства. На их основе варианты гипотетических условий синтезируются автоматически, но в предварительном виде. Для оценки их приемлемости с учётом знаний ПрО, не охваченных её описанием, и повышения содержательности дальнейший синтез выполняется интерактивно.

Обоснованы свойства правил синтеза. Их применение дополняет множество закономерностей, представленных в обрабатываемой пос-формуле, и гарантированно продолжает вывод в ситуациях неприменимости базового правила вывода в исчислении пос-формул.

Расширение первопорядкового исчисления пос-формул правилами синтеза преобразует его в исчисление дедуктивно-абдуктивного типа, свободное от ряда ограничений.

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

К перспективным направлениям дальнейшей работы относится анализ возможностей использования и развития полученных результатов:

• в области онтологий проектирования с порождением знаний шире, чем только в классе логических следствий известного, и с понижением, может быть поначалу, выразительности языка формализации для совместимости с другими разработками этой области;
• в задачах диагностики наблюдаемого с привлечением экспериментальных данных для поддержки экспертной оценки синтезируемых объяснений;

применительно к неклассическим логикам с семантикой конструктивности и немонотонности в приложениях компьютерных систем диагностики и поддержки принятия решений

About the authors

Stanislav N. Vassilyev

V.A. Trapeznikov Institute of Control Sciences of the Russian Academy of Sciences

Author for correspondence.
Email: vassilyev_sn@mail.ru
Scopus Author ID: 6603565134
ResearcherId: O-7577-2017

Doctor of Ph.D. , Chief Researcher ,  Academician of the RAS,  Member of the Russian Association of Artificial Intelligence (AI)

Russian Federation, Moscow

References

Supplementary files