Содержание к диссертации
Введение
Глава 1. Алгоритмизация силлогистики: история вопроса 11 - 28
1. Проблема моделирования (симуляции) «естественных» рассуждений 11-13
2. Восточные школы: силлогистика джайнов 13 -14
3. Античная мысль 14-17
Силлогистические исследования Аристотеля 14- 16
Перипатетики 16
Римский стоицизм 17
4. Средневековая силлогистика 17-18
5. Силлогистические исследования Нового времени 18 - 28
Труды по силлогистике Г. Лейбница 18-21
Система Г. Холланда 21 - 22
Работы С. Маймона, Ф. Кастильона, Ж. Жергонна 22 - 24
Логические идеи А. де Моргана 24
Силлогистические исследования Л. Кэрролла 24-26
6. Современные исследования в области негативной силлогистики 26 - 27
7. История алгоритмизации систем негативной силлогистики 27 - 28
Глава 2. Анализ систем негативной силлогистики 29 - 45
1. Обобщенная формулировка исследуемых систем негативной силлогистики 29 - 32
2. Натуральная система негативной традиционной силлогистики (нТС) 32-39
3. Натуральная система негативной силлогистики Больцано (нБС) 39 - 40
4. Натуральная система негативной силлогистики Кэрролла (нКС) 40-42
5 Натуральная система негативной силлогистики Аристотеля (нАС) 42 - 44
6. Натуральная система негативной фундаментальной силлогистики (нФС) 44-45
Глава 3. Описание алгоритма для натуральных систем негативных силлогистик 46 - 71
1. Сущность алгоритма 46
2. Общая характеристика алгоритма 47 - 61
Формализованный язык, используемый алгоритмом 47 - 48
Эвристики алгоритма 48-54
Алгоритмические процедуры 54-61
3. Общее описание алгоритма 61-63
4. Пример работы алгоритма 63 - 68
5. О программной реализации 68-70
6. Перспективы развития алгоритма 70-71
Заключение 72-77
Литература 78-82
- Восточные школы: силлогистика джайнов
- Силлогистические исследования Нового времени
- Натуральная система негативной традиционной силлогистики (нТС)
- Формализованный язык, используемый алгоритмом
Введение к работе
Актуальность темы исследования 4-5
Степень разработанности проблемы 5-8
Цель и задачи исследования 8 — 9
Научная новизна исследования 9
Тезисы, выносимые на защиту 9
Методологические основы и источники исследования 10
Практическая значимость 10
Апробация работы 10
Восточные школы: силлогистика джайнов
Несмотря на то, что негативная силлогистика является менее разработанной силлогистической теорией, чем, скажем, такая хорошо известная теория, как позитивная силлогистика, мыслители уже давно активно стали оперировать с так называемыми негативными терминами и исследовать условия истинности и ложности таких высказываний. Пожалуй, впервые стали это делать в джайнистской школе.
Как известно, джайнисты отрицали абсолютный характер знания и считали, что оно носит только вероятностный характер. Поэтому все ассерторические высказывания, исследуемые ими, содержат приставку «некоторым образом», которую с позиций современной науки можно назвать вероятностным оператором. Джайнистские ассерторические высказывания с вероятностным оператором «некоторым образом» содержат и негативные силлогистические термины: 1. Некоторым образом S есть P; 2. Некоторым образом S есть Р; 3. Некоторым образом S есть Р и также Р; 4. Некоторым образом S есть неописуемое; 5. Некоторым образом S есть Р и также неописуемое; 6. Некоторым образом S есть Р и также неописуемое; 7. Некоторым образом S есть Р и также Р и таюке неописуемое; Таким образом, мы видим начала аналитической мысли у джайнов, позволяющие рассматривать отрицательные предикаты, четко противопоставляя их утвердительным. В ходе рассуждений джайнистов можно проследить также апелляцию к троичной системе счисления, активно используемой в компьютерных приложениях математики на сегодняшний день. Джайны, как мы видим, рассматривали сам термин, его отрицание, а также неописуемое, т.е. то, относительно чего невозможно дать точную информацию.
Кроме того, как отмечается в работе В. А. Бочарова и В. И. Маркина «Введение в логику»23, последователи данного учения допускали, что к утверждению может быть прило-жимо сразу несколько характеристик и каждому указанному высказыванию соответствует самостоятельное истинностное значение, т.е. философы-джайнисты принимали принцип семизначное, полагая, что высказывание может иметь одно из следующих семи значений: «только истинно», «только ложно», «только неопределенно», «истинно и ложно», «истинно и неопределенно», «ложно и неопределенно», «истинно, ложно и неопределенно».
Еще один очень важный момент: джайны рассматривали высказывания с отрицательными предикатами как утверждения (в высказывательных формах везде стоит связка «есть»; как хорошо видно, отрицательная связка вообще отсутствует, что, видимо, объясняется философской концепцией джайнизма, согласно которой всякое свойство некоторым образом присуще любому классу или предмету). Эта идея - о рассмотрении высказываний с отрицательными предикатами как утвердительных - опередила мысль многих логиков Античности и Средневековья, исключая лишь Аристотеля.
Думаю, что возможно даже говорить о некоторых начатках неэкзистенциальной логики у джайнистов, когда наряду с реальными признаками рассматриваются и возможные, несуществующие предикаты, и «неописуемое», которое можно ассоциировать с универсальным термином. А вот отрицательных субъектов у джайнов еще не было. Первым этапом в исследовании систем негативной силлогистики явились работы Аристотеля, в которых ученый сформулировал ряд важных идей. После Аристотеля средневековые мыслители заложили фундамент традиционной силлогистики, которая легла в основу большинства современных теорий. Однако многие силлогистические системы, как средневековых логиков, так и их последователей эпохи Возрождения, Нового и даже Новейшего времени бедны на негативные фрагменты.
Возможно, причиной этому послужило то обстоятельство, что негативный термин в традиционных силлогистических теориях трактуется как дополнение к позитивному термину до универсума рассуждения. Но точно таким же образом трактуется и отрицательный предикат. Следовательно, выражения «не есть Р» и «есть Р», где « Р» - негативный термин — рассматриваются как эквивалентные. Поэтому в данных логиках справедливо следующее метатеоретическое утверждение: -(а есть Р) = (а не есть Р) = (а есть Р). Отсюда происходит как «избегание» негативных терминов, так и некоторая нечеткость в алгебраическом построении негативных силлогистик у ряда логиков Нового времени. Но о данном обстоятельстве будет сказано позже.
Однако вернемся к Аристотелю. В 46-ой главе первой книги «Первой Аналитики» Аристотель исследует вопрос, имеют ли одинаковое значения выражения «не быть этим» и «быть не этим», и отвечает следующим образом: «быть не белым» и «не быть белым» - совсем не одно и то же, так как отрицание -{а есть Р) относится к связке «есть», но никак не к логическому сказуемому «Р». Эта же позиция развивается им в трактате «Об истолковании».
Таким образом, Аристотель полагает, что выражения «а есть Р» и «а есть Р» суть утверждения, а «а не есть Р» и «а не есть Р», - соответственно, отрицания. Итак, качество силлогистических высказываний определяется Стагиритом исключительно по связке «есть» («не есть»). Так как логика Аристотеля является неэкзистенциальной 5, то предикат «есть Р» есть дополнение к «есть Р» не до всего универсума рассмотрения, а только до универсума реально существующих объектов; предикат же «не есть Р» является дополнением как раз до всего универсума исследования, включающего как реальные, так и виртуальные объекты. Поэтому Стагирит принимает выводимости лишь в одну сторону: а есть Р = а не есть Р; а есть Р = а не есть Р. Обобщая данные выкладки с помощью средств современной формальной логики, можно говорить только о превращении утвердительных высказываний в отрицательные, но не наоборот: SaP = Se P, Sa P = SeP, SiP = So P, Si P = SoP. Обратные соотношения в системе Аристотеля категорически неверны. Перипатетики В дальнейшем проблематика негативной силлогистики разрабатывалась в перипатетической школе. Одним из видных ее представителей являлся Феофраст, чьи работы также затрагивали область силлогистики с отрицательными терминами. В частности, у него появляются отрицательные субъекты. Вот пример одного из умозаключений, исследуемых Феофрастом: Всякий S есть Р Всякий S есть R Некоторый Р есть некоторый R. Здесь Феофраст квантифицирует и предикат суждения, ставя кванторные выражения, в частности, «некоторый», непосредственно перед логическим сказуемым. Хотя данный силлогизм (если отвлечься от квантификации предиката) не проходит в ряде силлогистических систем, например, в системе Аристотелевской силлогистики, он представляет собой интерес тем, что явно указывает на оформление идеи традиционной логики, где он верен.
Однако, несмотря на, казалось бы, явное использование отрицательных предикатов и субъектов, операция отрицания термина не была еще эксплицирована и применялась всеми исследователями неявно, интуитивно.
Силлогистические исследования Нового времени
Следующим важным этапом в формировании негативных силлогистических теорий стала система Лейбница. На современном языке формальной логики алгебраическая семантика Лейбница для атрибутивных категорических высказываний записываются следующим образом: SaP = (S-P = 0) SeP = (S-P = 0) SiP = (S-P Ф 0) SoP (S-P ф 0) Современная операция логического умножения «» задавалась Лейбницем так: А est В, A est С Ь- A est ВС, где «est» обозначало связку «есть», а ВС - логическое произведение. Сами же семантические определения силлогистических высказываний записывались, к примеру, следующим образом: определение 1 имело вид «S est Р aequivalent S non-Р», где «aequivalent» - «эквивалентно», «поп», соответственно, означает «не», а операция логического умножения попросту опускалась.
Даже у Лейбница мы видим явно проявившееся средневековое смешение отрицательных предикатов и негативных терминов; в частности, в определении 1 отрицательный предикат «не есть Р», составляющий пустое произведение с логическим подлежащим, записывается и самим Лейбницем как отрицательный термин («non-Р», или « Р», в современном варианте).
Заслуживает внимания стремление Лейбница обосновать все правильные модусы, используя в качестве исходных правил модус Barbara и принцип противоречия (например, так ученый обосновывает модус Bocardo). Эта возможность была отмечена уже в работах самого Аристотеля. Тем не менее, данное стремление Лейбница можно рассматривать как попытку построения силлогистического исчисления на новой основе.
Еще более интересной идеей является мысль о гомоморфном соответствии между простыми силлогистическими терминами и рядом целых чисел - так называемая арифметизация силлогистики. Хотя арифметизация силлогистики напрямую не коррелирует с исследуемой нами задачей, ее можно рассматривать как достаточно успешную попытку алгоритмизации для целого класса законов и модусов силлогистики.
В результате наряженных творческих поисков («Элементы универсальной характеристики», «Элементы универсального исчисления» и «Исследования универсального ис числения», «Элементы исчисления» и «Правила, по которым можно с помощью чисел судить о правильности выводов, о формах и модусах категорических силлогизмов») Лейбниц сформулировал суть данного приписывания следующим образом: субъекту силлогистического высказывания ставится в соответствие произвольная упорядоченная пара целых чисел +а, -Ь , где обязательно «а и b должны быть взаимно простыми, т.е. не иметь общего делителя»27, а предикату, в свою очередь, отличная от первой упорядоченная пара +с ,-d , обладающая аналогичными первой свойствами. Общеутвердительное силлогистическое высказывание истинно тогда и только тогда, когда +а без остатка делится на +с и -Ь без остатка делится на -d. Иначе истинным считается частноотрицательное высказывание. Частноутвердительное высказывание истинно тогда и только тогда, когда а и d, а также b и с являются взаимно простыми числами. В противном случае истинно общеотрицательное высказывание. Сложным терминам приписывались произведения их составных частей. Например, запись A est В, A est С Ь- A est ВС, где «est» обозначало связку «есть», а ВС - логическое произведение, может быть корректно проинтерпретирована следующим образом: (14-9) est (7-3), (14-9) est (2-1) I- (14-9) est (14-3). Как нетрудно заметить, при правильной интерпретации истинных посылок заключение также получается высказыванием, подпадающим под условия истинности указанной интерпретации.
Используя данный прием, Лейбниц в первую очередь протестировал данную модель на законах логического квадрата и обращения, а впоследствии он применил ее к более сложным силлогистическим утверждениям — силлогистическим модусам. Оказалось, что в ней истинны все 24 правильных модуса. Однако корректные с арифметической точки зрения результаты получаются и для неправильных модусов. Последнее досадное обстоятельство осложняется еще и тем, что с алгоритмической точки зрения Лейбниц не обнаружил эффективной стратегии поиска опровергающих некорректные модусы пар (т.е. таких упорядоченных пар взаимно простых чисел, которые бы правильно арифметизиро-вали противоречащие друг другу высказывания вида SaP, SoP и SeP, SiP). Может быть, поэтому столь продуктивная идея алгоритма проверки силлогистических доказательств далее не разрабатывалась ученым. Современные логики (Бахтияров К. И.) успешно построили алгоритм на базе идеи арифметизации и реализовали его в виде компьютерных программ КЭРРОЛЛ, БУЛЬ и СОРИТ, активно опирающихся на векторную семантику трехзначной логики. Однако именно Лейбниц положил начало силлогистическим исчислениям в их современном понимании. Система Г. Холланда Следующим этапом в развитии силлогистических теорий с использованием негативных терминов стали работы немецкого ученого Г. Холланда, во многом развивавшиеся благодаря полемике с другим немецким ученым И. Ламбертом, занимавшимся силлогистикой, в том числе и негативной как исключительно арифметической системой (термины - параметры, силлогистические операторы выражались им через арифметические операции).
Правда, и здесь приходится сделать важное замечание о том, что различий между отрицательным предикатом и отрицательным термином не проводилось. Впоследствии у ряда исследователей, интерпретировавших силлогистические высказывания с использованием инструментария теории классов и не проводивших этого важного различия, операция взятия дополнения к некоторому классу, представлявшему объем силлогистического термина, и операция терминного отрицания слились воедино, что привело к некоторым неточностям в их логических построениях.
Натуральная система негативной традиционной силлогистики (нТС)
Для удобства использования данных правил в программной реализации алгоритма будем использовать вместо знака импликации символ « », а вместо знака дизъюнкции -символ «V». Правила 1—3, 6, 16, 17, 25, 28, обеспечивающие введение новых логических операторов (логических и терминных констант), а потому могут быть названы повышающими ранг формулы. Доказательством в нТС будем называть вывод формулы А из пустого множества формул Г. Для доказательства семантической непротиворечивости и полноты системы нТС докажем дедуктивную эквивалентность систем ТС и нТС. Их дедуктивная эквивалентность будет означать тот факт, что они описывают одно и то же. Так как относительно системы ТС посредством ее погружения в логику предикатов доказана семантическая полнота и непротиворечивость , то данные свойства будут справедливы и относительно нТС. Докажем сначала Лемму 2.2.1: УА(Г Тс Ь А = Г „ тс -А). Для доказательства Леммы 2.2.1 необходимо и достаточно показать, что все аксиомы ТС являются теоремами нТС, а также, что правило modus ponens сохраняется в нТС. Доказательство данной Леммы приведено в Приложении 1.
Затем докажем Лемму 2.2.2: V А(Г „тс I- А = Г тсЬ А). Напомним, что если Г пусто, то мы имеем дело с доказательством, а не выводимостью. Доказательство Леммы 2.2.2. Лемма 2.2.2: Пусть имеется вывод в системе нТС некоторой формулы А из множества посылок Г (возможно, что Г = 0; тогда мы имеем дело с-доказательством). Сі Ck Ск графически равно А. Пусть Aj - это множество допущений (под допущениями будем понимать как заданные допущения - посылки, входящие в множество Г, — так и произвольные допущения), не исключенных из вывода на шаге і. (Данное множество может быть пустым). Тогда в аксиоматическом исчислении А, Ь-тс С,-. Докажем методом возвратной математической индукции, что данная выводимость действительно имеет место, для любого i: 1 i к. Индукция будет вестись по номеру формулы в выводе/ доказательстве в системе нТС. Сформулируем индуктивное допущение (ИД): Пусть наша лемма верна для всех формул вывода с номером, строго меньшим і. Покажем, что она верна и для формулы с номером і. Доказательство разбивается на б главных случаев, которые, в свою очередь, разбиваются на подслучаи (по числу правил системы нТС). По ИД, справедливы утверждения: Aj I- тс Cj, Am Ь-тс Cm. На шаге і-1 все допущения из Aj и Ат не исключены из вывода, поскольку, по определению вывода, они могли быть исключенными из него только вместе С Cj.
Относительно номеров формул справедливо: j m, либо j m, либо j = m, по определению вывода в системе нТС. Следовательно, также по определению вывода в нТС, Aj Am, либо Amc Aj5 либо Aj = Am. Отсюда (и по определению вывода) AjUAra Ац. Но так как применение правил данной группы не вызывает исключения из вывода каких-либо допущений, то AjU Am ді# Отсюда и из ИД, а также по свойству монотонности классической выводимости следует, что: AjU Am I- тс Cj и, в итоге, Aj Ь- тс CJ; AJU Ага Ь- тс Ст и, в итоге, Aj І- тс Ст. Покажем теперь, что для каждого правила данной группы Ail— тс Cj. Предположим, что С; получена по правилу вывода № 29. Тогда А; I- „тс XaY. Тогда, по ИД, справедливы утверждения: Aj Ь- тс XaZ; и Ат Ь- тс ZaY. Из вышеприведенных рассуждений делаем вывод, что А; I- тс XaZ; и А; I- тс ZaY. Для аксиоматической системы справедливо Ь-тс (XaZ&ZaY) ZD XaY (TCI). Отсюда верно, что Aj Ь-тс (XaZ&ZaY) з XaY. В аксиоматической системе выводимо Ь-тс XaZD(ZaYD(XaZ&ZaY)) (одна из аксиом ТСО). Отсюда Д;Ь-Тс XaZD(ZaYD(XaZ&ZaY)). Затем 2 раза применяем modus ponens и в итоге имеем: А; Ь-тс XaZ&ZaY. Еще раз применяем modus ponens и получаем Aj Ь- тс XaY.
Совершенно аналогично рассуждаем для оставшихся двухпосылочных правил с №№ 7, 8, 30. Соответствующие утверждения в аксиоматической системе для пропозициональных правил вывода (№№ 7-8) считаем доказанными, а доказательство аксиоматического утверждения для силлогистического п.в № 30 I—re (XaZ&ZeY)3XeY приводится в Приложении 2. Случай 6. Пусть С; получена по правилу вывода №28. Тогда А; 1-„тс - С, где С -последнее допущение в выводе. Все формулы, начиная с последнего допущения С и вплоть до результата применения правила №28, исключены на і-том шаге из дальнейших шагов построения вывода. Для доказательства семантической непротиворечивости и полноты системы нБС докажем дедуктивную эквивалентность систем БС и нБС. Их дедуктивная эквивалентность будет означать тот факт, что они описывают одно и то же. Так как относительно системы БС посредством ее погружения в логику предикатов доказана семантическая полнота и непротиворечивость4 , то данные свойства будут справедливы и относительно нБС. Для доказательства семантической непротиворечивости и полноты системы нБС докажем дедуктивную эквивалентность систем КС и нКС. Их дедуктивная эквивалентность будет означать тот факт, что они описывают одно и то же. Так как относительно системы КС посредством ее погружения в логику предикатов доказана семантическая полнота и непротиворечивость42, то данные свойства будут справедливы и относительно нКС. Данная аксиоматическая система (назовем ее кратко АС) также является системой со схемами аксиом, поэтому правило подстановки нам не требуется. Понятия вывода и доказательства в АС и нАС определяются аналогично соответствующим понятиям для ТС и нТС. Данная аксиоматическая система (назовем ее кратко ФС) также является системой со схемами аксиом, поэтому правило подстановки нам не требуется. Понятия вывода и доказательства в ФС и нФС определяются аналогично соответствующим понятиям для ТС и нТС. Для доказательства семантической непротиворечивости и полноты системы нФС докажем дедуктивную эквивалентность систем ФС и нФС. Их дедуктивная эквивалентность будет означать тот факт, что они описывают одно и то же. Так как относительно системы ФС посредством ее погружения в логику предикатов доказана семантическая полнота и непротиворечивость46, то данные свойства будут справедливы и относительно нФС.
Формализованный язык, используемый алгоритмом
На мой взгляд, значимым фактом является то обстоятельство, что техника поиска вывода практически не отличается от техники вывода в самих исследуемых натуральных силлогистических исчислениях. Это отличие, экономящее время работы алгоритма и делающее его более компактным, основано на значительном сокращении множества меток. Метки, введенные и используемые Болотовым А.Е., Бочаровым В.А., Горчаковым А.Е., Шангиным В.О. и др ., не применяются. Таким образом, у меня в качестве меток используется конечное подмножество множества целых чисел, а также метка - , которая применяется при «вычерпывании» из множества формул вывода тех и только тех формул, которые необходимы и достаточны для построения вывода или доказательства.
Алгоритм принципиально строится как открытая система, к которой пользователь может приложить потенциально бесконечное множество текстовых пакетов, содержащих новые силлогистические правила вывода. К данным пакетам предъявляется только одно требование: все они должны быть написаны на стандартном формализованном языке, чтобы алгоритм смог их прочитать и начать корректную работу в предложенных ему дедуктивных системах. Формализованный язык, используемый алгоритмом Все правила вывода той или иной натуральной системы, с которой работает алгоритм, должны быть записаны на стандартном формализованном языке. Примеры записи дедуктивных постулатов на данном языке мы приводили, когда указывали правила вывода силлогистических систем в Главе 2. Опишем данный язык. Если правило вывода пропозициональное - т.е. в нем не затрагивается внутренняя структура высказываний, - то его посылки и заключение записываются с помощью мета-переменных для формул (см. Главу 2). Если правило вывода является прямым, то для его записи используются метапеременные А,В, А\, Bj, А2--. Если же оно непрямое, то нам следует использовать метапеременные А,В,С, D, Aj, BJ,CJ, Dj, А2 — , причем литерами С и D с индексами будут обозначаться допущения, а литерами А и В с индексами- формулы вывода, отличные от указанных допущений. Если же правило вывода затрагивает внутреннюю структуру формул, то для его записи на указанном языке мы используем метатермы X, Y, Z с индексами. Далее, для отделения посылок друг от друга мы используем технический символ «,», а для разграничения посылок и заключения - символ «К». Каждая запись, опреде- ляющая правило вывода, не содержит пробелов. Записи отделяются друг от друга техническим (служебным) символом новой строки. Пользователь сам может определить технические символы и способы демаркации, только данное определение должно быть явным для обеспечения четкой и однозначной работы алгоритма и программного модуля, соответственно. Отметим, что мы можем записывать правила вывода с пробелами, только в этом случае в программный модуль должна быть встроена функция удаления пробелов, чтобы не создавать лишних трудностей при работе программы. Пробелы в правилах вывода и формулах в данном тексте используются исключительно для удобства чтения.
Затем, для того чтобы систематизировать действия нашего алгоритма, мы приняли следующие условия относительно формулировки правил вывода. Если исходное правило (или аксиома) системы затрагивает внутреннюю структуру составляющих его простых высказываний и его заключение содержит конъюнкцию, то в исследуемой натуральной системе оно разбивается на два правила, каждое из которых содержит те же посылки, что и исходное, а заключения являются левым и правым конъюнктами, соответственно. Например, аксиому SoP = (-iSaP & SiS) следует разбить на два правила вывода: XoY Ь--nXaY и XoY h ХіХ.
Если же исходное правило (аксиома) затрагивает внутреннюю структуру входящих в его состав простых высказываний и одна из его посылок является конъюнктивной, то она заменяется двумя посылками, представляющими собой конъюнкты первоначальной посылки. К примеру, трансформируем аксиому (SeP & SiS) ZD Sa P в правило вывода XeY, ХіХ (- Xa Y. Допустимость подобного рода трансформаций обосновывается путем обращения к классической логике высказываний (подробно о правомерности таких преобразований и их строгом обосновании мы говорили выше в Главе 2, когда строили натуральные силлогистические исчисления для соответствующих аксиоматических систем). Дополнительные примеры записи правил вывода в натуральных силлогистических системах на указанном формализованном языке приводятся в Главе 2. Эвристики алгоритма Помимо открытого уровня дедуктивных правил в алгоритме существует еще один открытый уровень - уровень сложности используемых программой эвристик. Эвристики позволяют «просеивать» формулы, создающие пространства состояний, и «высаживать» в поисковое поле программы только полезные, «творческие» формулы, отбрасывая те, которые «прорастут сорняками», т.е. формулы лишние и тормозящие работу компьютера. Разъясним данное утверждение. Если у нас в произвольной системе есть правило, которое позволяет наращивать терминную сложность заключения по сравнению с тер-минной сложностью посылок (понятие терминной сложности разъяснено ниже), то такое правило позволяет строить потенциально бесконечные объекты, если его ничем не ограничить сверху. Например, возьмем правила XaY Ь- Xe Y и XeY Ь- Xa Y и посылку SaM. С помощью этих правил получаем такой ряд конструктивных объектов: Se M, Sa—М, Se- М, Sa М и т.п. Очевидно, что данный ряд стремится к бесконечности и делает невозможной работу любого алгоритма. Помня о том, что не следует умножать сущности без необходимости, мы можем ввести следующее аналитическое ограничение на объекты такого вида: глубина данных объектов не должна превышать некоторого заданного значения специальной переменной. Обозначим указанную специальную переменную как п. Она может принимать значения от 0 до k, к Є Z. Тогда нулевое значение переменной п будет означать самое простое, минимальное пространство состояний, на котором проводится поиск вывода или доказательства (или соответственно, опровержения некорректной формулы); на построение конструктивных объектов указанного типа налагается запрет. При п = 1 данное пространство состояний расширяется и в него включаются формулы первого уровня повышенной терминной сложности (т.е. формулы, полученные в результате однократного применения таких «конструктивных» правил и содержащие не более 1 символа терминного отрицания). При п = 2 поисковое пространство состояний расширяется еще больше, и теперь допускается использование формул второго уровня терминной сложности. Вообще, при п - к в зону поиска включаются формулы k-ого уровня сложности, построенные с помощью правил описанного выше типа. В программной реализации алгоритма пользователю автоматически предлагаются эвристики уровня 0-2 в виде флажков выбора. Если данных эвристик недостаточно, пользователь может сам задать эвристику необходимого терминного уровня сложности.
