диссертация модальная логика

-201 -

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

Существуют способы доказательств, основанные на методе резолюций. Они интересны тем, что дают возможность использовать средства автоматического доказательства, применяемые в логическом программировании [39, 90, 91, 103].

5.4.3 С р а в н е н и е с т а н д а р т н о й и к л а у з а л ь н о й ф о р м л о г и к и

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

5.4.4 П е р е в о д в к л а у з а л ь н у ю ф о р м у

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

Суть подобного перехода заключается в выполнении ряда преобразований [39, 103, ПО].

- 2 0 2 -

Сначала импликации и эквивалентности представляются в терминах

отрицания, дизъюнкции и конъюнкции на основании следующих правил:

[ X - ^ Y ] < ^ - п X v Y
[X о> У ]		<-> (X -> У ) & ( У	X)
[X	У ]	о (^Х V У ) & ( ^ У	V X )

Когда импликации и эквивалентности преобразованы к новой форме,

оставшаяся часть приведения состоит:

1. Из перенесения отрицаний внутрь предложений за конъюнкции,

дизъюнкции и кванторы до тех пор, пока они не окажутся непосредственно

перед атомарными формулами.

Это достигается путем многократного применения таких правил

эквивалентности:

-,(Х & У )	-пХ V ^ У
^ ( Х V У ) ^ ^ Х & - . У
-п ЭУ Х ( У ) ^	У У -ПХ(У)

^У У . Х ( У ) О З У ^ Х ( У )

-, - п Х ^ Х ,

где X и У - являются формулами, а V - произвольная переменная.

2. Передвижения дизъюнкций внутрь предложений за конъюнкции и кванторы до тех пор, пока, они не станут связывать лишь атомы и атомы с отрицаниями.

[ У & 2] V X о [ У V X] & [2 V X]

Зv Y v X < ^ З v [ Y v X ]

УУ У V X <-> У У [ У V X]

где V не встречается в X .

-203 -

Приведенные эквивалентности существенны для преобразования любого

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

3. Устранение кванторов существования.

Исключение кванторов существования приводит к предложениям, которые

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

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

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

предложений вида:

УУ1\/У2	... \/Уп ЭиХ, принадлежащих 8.
Такое предложение может быть заменено новым:
\ / У 1 \ / У 2	... \/Уп X ' ,
где X ' получено из X заменой всех свободных вхождений и в X на терм
/ ( V , , ...,у„),	где f - есть некоторый функциональный символ, не встречающийся

в 8 ( / ( У 1 , ...,v„) называется функцией Сколема).

Если п=0, то терм сводится к константному символу. Заметим, что замена не является эквивалентной и применима только к предложениям, а не к формулам. Новая конъюнкция (множество предложений) является совместным или несовместным, если и только если 8 является таковым.

Для того чтобы преобразовать предложения, входящие в 8, к корректному виду, полезно передвинуть кванторы общности внутрь конъюнкций:

У У ( Х & У) ^ У У Х & У У У .

4. Перезапись дизъюнкции атомов и их отрицаний.

- 2 0 4 -

A , V ... V Ат v ^ B ь	..., -пВп
в виде клауз:
А1У ... V Ап, < - В ь	..., Вп
Это достигается путем повторного применения приведенных выше правил.
Приведенные формулы составляют логическую		часть семейства
алгоритмов для приведения стандартной формы к клаузальной.
5.4.5 М е т о д	р е з о л ю ц и и и ф о р м и р о в а н и я	л о г и ч е с к о г о
с л е д о в а н и я

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

Этой задаче соответствует задача, рассматриваемая в исчислении		предикатов,
когда ищется возможность	доказательства того, что некоторая	правильно
построенная формула (ППФ)	логически следует из некоторого множества 8

правильно построенных формул. Рассмотрим этот вопрос подробно.

Втипичной задаче на доказательство теорем имеем множество 8 ГШФ, исходя из которого нам нужно доказать некоторую целевую ППФ \ ¥ . Системы, основанные на резолюции, предназначены для доказательства путем построения противоречия или опровержения. При таком опровержении сначала берется отрицание целевой ППФ и добавляется к множеству 8. Это расширенное множество затем преобразуется во множество предложений, после чего резолюция используется при попытке вывести противоречие, представляемое пустым предложением М1Ь.

Впользу процесса доказательства путем опровержения Нильсон Н. [ПО] приводит следующее утверждение. "Предположим, некоторая ППФ W логически следует из некоторого множества 8 правильно построенных формул, тогда по определению каждая интерпретация, удовлетворяющая 8, также

- 2 0 5 -

удовлетворит и W. Никакая интерпретация, удовлетворяющая S, не может удовлетворять (-iW) и, следовательно, никакая интерпретация не может удовлетворять объединению S и (-iW). Множество ПНФ, которое не может

удовлетворять ни при какой интерпретации, называется неудовлетворимым. Таким образом, если W логически следует из S, то множество S и (-iW) является неудовлетворимым".

Можно показать, что если резолюция многократно применяется к некоторому неудовлетворимому множеству предложений, то, в конце концов, будет построено пустое предложение, NIL . Так, если W логически следует из S, резолюция, в конечном счете, создаст пустое предложение из предложения Su(-iW) в виде предложений. Обратно, если из предложения в виде

предложений для множества			S и (-iW)	порождается	пустое предложение, то
можно показать, что W.логически следует из S [110].
Можно считать оправданным поиск подхода к					использованию метода
резолюций в процессе формирования образа объекта проектирования.
5.5	О п и с а н и е	о б р а з а	о б ъ е к т а	п р о е к т и р о в а н и я с р е д с т в а м и
и с ч и с л е н и я п р е д и к а т о в п е р в о г о п о р я д к а и я з ы к а П р о л о г
Под	описанием	образа объекта проектирования			в терминах исчисления

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

Возможные схемы перехода от знаний профессионала к некоторому формализму можно представить в следующем виде:

1.Знания профессионала - исчисление предикатов первого порядка - клаузальная логика - Пролог.

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

- 206 -

Сейчас мы с уверенностью можем сказать, что, осуществив указанные

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

может приравниваться к заключительному этапу процесса					формирования
концептуального образа объекта проектирования.
5.5.1	С х е м а	" З н а н и я	п р о ф е с с и о н а л а	-	и с ч и с л е н и е

п р е д и к а т о в п е р в о г о п о р я д к а - к л а у з а л ь н а я ф о р м а л о г и к и - П р о л о г "

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

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

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

порядка.

Для осуществления этого пути имеющиеся категорические суждения

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

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

представить в нотации, требуемой в Прологе.

Основные для силлогистики формы высказываний [ПО, 111] в исчислении

предикатов записываются так:

- общеутвердительное суждение А - Всякий S есть Р

V x ( S ( x ) Р ( х ) )	(5.1)
- общеотрицательное суждение Е - Никакой S не есть Р
Vx(S(x) -> -пР(х))	(5.2)

-2 0 7 -

-частноутвердительное суждение J - Некоторый S есть Р

3x(S(x) & Р(х))	(5.3)
- частноотрицательное суждение О - Некоторый S не есть Р
3x(S(x) & (Р(х))	(5.4)

Приступим к практическому осуществлению указанных преобразований. Сначала введем предикаты:

W0Алтайдизель(Х)

W1 - удовлетворяет_требованиям(Х)

W2требует_доработки(Х)

W3 - производительность_трактора(Х)

W4повыщенный_запас_крутящего_момента(Х)

W5регулировка_на_2_уровня(Х)

W6модификации_без_изменения_базы(Х)

W7наименьшие_затраты_на_ТО(Х)

W8требования_эргономики(Х)

W9высокий_ресурс(Х)

W10нормы_экологии(Х)

W11низкая_начальная_стоимость(Х)

W12мин_расход_топлива_и_масла(Х)

W13 - многотопливный(Х)

W14многоцелевой(Х)

W15 - мин_металлоемкость(Х)

W16приспособленный_к_АСУ(Х)

Запись бинарных высказываний в стандартной форме получается путем замены предикатов S(x) и Р(х) в формулах (5.1) - (5.4) на предикаты из приведенного списка в соответствии с формой утверждения. Таким образом, полученное определение выглядит следующим образом:

Vx(выcoкиЙJpecypc(X) -> удовлетворяет_требованиям(Х))

- 2 0 8 -

\/х(производительность_трактора(Х)-^ удовлетворяет_требованиям(Х)) \/х(наименьшие_затраты_на_ТО(Х)-^ удовлетворяет_требованиям(Х)) \/х(многотопливный(Х) -> удовлетворяеттребованиям(Х))

\/х(удовлетворяет_требованиям(Х) -> многоцелевой(Х))

\/х(повышенный_запас_крутящего_момента(Х)-^произв-сть_трактора(Х))

\/х(регулировка_на_2_уровня(Х) нормы_экологии(Х))

\/х(мин_расход_топлива_и_масла(Х) -> нормы_экологии(Х)) \/х(модификации_без_изменения_базы(Х)^ низкая_нач_стоимость(Х)) Ух(многотопливный(Х) -> - 1 низкая_начальная_стоимость(Х))

Эх(низкая_начальная_стоимость(Х) - i многоцелевой(Х))

Зх(Алтайдизель(х) & удовлетворяет_требованиям(Х)) Зх(Алтайдизель(х) & мин_металлоемкость(Х))

Зх(многоцелевой(х) & мин_металлоемкость(Х)) Зх(регулировка_на_2_уровня(х) & - i требует_доработки(Х)) Зх(высокий_ресурс(х) & - i требует_доработки(Х))

Для получения клаузальной формы преобразуем формулы (5.1)-(5.4) в

соответствии с вышеприведенными правилами:

\/x(^S(x)vP(x)
P(x)^S(x)	^ •
Уx(^S(x)^y^P(x)
^P(x)&S(x)
3x{Six)&P(x)
S(A)&P(A)
3x{Six)Sc-.P{x)
S(A)&-.P(A)

В ( 5 . 7 ) и ( 5 . 8 ) А - сколемовская константа.

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

- 2 0 9 -

Таблица 5.1 - Представление знаний об объекте проектирования в клаузальной форме логики

Тип	Символь­
суаде-	ное пред­	Клаузальная форма логики
ния	ставление
А	W10W\	удовлетворяет требованиям(Х)	высокий ресурс(Х)

Аудовлетворяет требованиям(Х) <- производительность трактора()

А	w^wl	удовлетворяет требованиям(Х) <г- наименьшие затраты на ТО(Х)
А	W13W1	удовлетворяет требованиям(Х) <- многотопливный(Х)
А		многоцелевой(Х) <- удовлетворяет		требованиям(Х)
А	W4W9	производительность_трактора(Х) <-
		повышенный запас крутяш,его момента(Х)
А		нормы экологии(Х) <-регулировка		на 2_уровня(Х)
А	W12W9	нормы экологии(Х) <-мин расход		топлива и масла(Х)
А	W6W11	Низкая начальная стоимость(Х) <- модификации без изменения базы(Х)
Е	W13W11 •«-низкая начальная стоимость(Х),модификации без изменения ба-зы(Х)
Е	W14W11 <- многоцелевой(Х), низкая начальная стоимость(Х)
1	W0W1	Алтайдизель(а) & удовлетворяет требованиям(а)
1	W0W2	Алтайдизель(а) & мин	металлоемкость(а)
1	W15W14 Многоцелевой(а)&мин		металлоемкость(а)
0	W5W2	Регулировка на 2_уровня(а) & -1требует доработки(а)
0		высокий ресурс(а) & -1требует доработки(а)

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

клаузами Хорна - клаузами, содержащими не более одного утверждения.

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

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

рассматриваемого	перехода	выполняется	приведенная	ниже
последовательность действий.

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

- 2 1 0 -

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

Например, W 1 : - W 3 , W 7 , W 1 0 , W 1 3 .

Что означает, что W 1 выполняется, если выполняется и W 3 , и W 7 , и W 1 0 , и W 1 3 . Логическая интерпретация следуюпдая: W 1 - истинно, если истинно и

W 3 , H W 7 , H W 1 0 , H W 1 3 .

2.Для суждения Е предикаты можно менять местами в соответствии с формулой:

Vx(S(x) - » ^Р(х)) о Vx(^P(x) ^ S(x))

Отрицание в Прологе имеет имя not, и для указания отрицания какого-либо выражения Р используется запись not(P). Однако может возникнуть проблема записи негативного утверждения, так как отрицание в Прологе может использоваться внутри правила (в теле правила) и в качестве запроса (отрицание целевого утверждения). Поэтому отрицание требуется вводить в

тело уже существуюгцих правил.

3.Некоторые осложнения возникают при представлении высказываний типа J, О.

При устранении квантора существования вводится сколемовская функция или константа. Теоретически здесь не возникает никаких вопросов. Однако практическое назначение этой функции остается не совсем ясным.

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

Внутри программы все переменные связаны квантором всеобщности. Запрос же предполагает факт существования. Тогда, чтобы получить ответ на вопрос о существовании некоторого объекта с указанным свойством, нужно создать запрос Пролог-системе. А для того, чтобы убедиться, что предикат