Лекции - Системы искусственного интеллекта
Подождите немного. Документ загружается.
12.ПОЛНОТА И НЕПРОТИВОРЕЧИВОСТЬ ИСЧИСЛЕНИЯ
На основе введенных определений полноты и
непротиворечивости логические исчисления можно поделить на
следующие группы: полные и непротиворечивые; неполные и
непротиворечивые; противоречивые.
Наша задача – построение неклассических исчислений,
которые относятся к первым двум группам. Заметим, что на
практике полнота исчислений является желательным, но редко
удовлетворяемым фактором. Объясняется это многими
причинами, среди которых доминирующими являются следующие
две.
Размерность задач для конкретных сред (число
переменных, констант, предикатов, функций), для которых
имеет смысл использовать логические исчисления, как
правило, велика. Полное исчисление требует полной
аксиоматизации. Это приводит к большому росту числа
необходимых аксиом даже для сравнительно простых сред и
необходимости обоснования достаточности этих аксиом.
Число типов выводимых формул (целей) для реальной среды
ограничено конкретными потребностями. Вывод только этих
формул следует гарантировать, ограничиваясь тем множеством
аксиом, которые позволяют сделать.
Проблемой полноты и непротиворечивости исчислений
занимались и продолжают заниматься. Для некоторых
исчислений вопрос о полноте имеет положительный ответ,
например для классического исчисления высказываний и для
классического исчисления предикатов первого порядка. Для
классического исчисления предикатов вопрос полноты был
решён немецким математиком Куртом Геделем в 1930-1931
годах. Он доказал теорему, которая называется теоремой о
полноте классического исчисления логики предикатов первого
порядка. Согласно этой теореме любая общезначимая формула
классического исчисления логики предикатов первого порядка
выводима в этом исчислении. Это означает, что для
классического исчисления логики предикатов первого порядка
существует полная стратегия вывода.
Гедель доказал теорему о полноте классического
исчисления предикатов первого порядка, но не привёл полной
стратегии вывода, которую можно достаточно эффективно
использовать на практике. Это сделал в 1965 г. Дж.
Робинсон, опубликовав полную стратегию вывода для
классического исчисления высказываний на основе правила
резолюции. Заметим, что упомянутые положительные ответы о
полноте относятся к классическому исчислению предикатов
первого порядка. Нас же в практическом плане интересуют,
прежде всего, неклассические исчисления. Вопрос об их
полноте и непротиворечивости обсудим далее. Однако ещё раз
заметим, что неклассические исчисления, использующие
классическое исчисление предикатов первого порядка, могут,
наряду с другими, включать его правила вывода, в частности
правило резолюции. Вследствие теоретической и практической
значимости этого правила стратегию вывода на его основе
рассмотрим детально в последующем.
Отметим ещё один важный момент, который связан с
теоремой о полноте классического исчисления логики
предикатов первого порядка и вопросом об установлении факта
невыводимости формулы из начальной базы знаний без вывода.
Теорема Геделя гласит, что любая общезначимая формула
логики предикатов первого порядка выводима в классическом
исчислении логики предикатов первого порядка. Но в каждом
конкретном случае до тех пор пока вывод не осуществлен, мы
не знаем, выводима ли данная формула. А если она не
выводима и, следовательно, вывод никогда не будет найден,
то как отличить ситуацию, когда мы ещё не достигли вывода,
от ситуации, когда он никогда не будет достигнут? К
сожалению, ответ на этот вопрос не утешителен: невозможно
различить эти две ситуации и выводимость формулы может быть
установлена только тогда, когда она выведена. Если же она
не выводится, то придется осуществить все варианты вывода и
только после этого, если она всё-таки не была выведена,
сделать заключение о невыводимости. Это же считается
справедливым и для неклассических исчислений.
Как следствие, неутешительным остаётся ответ и на
вопрос распознавания противоречивости исчисления: для того
чтобы установить непротиворечивость исчисления в общем
случае, придётся осуществить вывод всех теорем и только при
отсутствии среди них любых двух, одна из которых является
отрицанием другой, сделать заключение о непротиворечивости
исчисления.
92
13.ВЫВОД НА ОСНОВЕ ПРАВИЛА РЕЗОЛЮЦИИ
Правило резолюции (или резолюция) уже рассматривалось.
это правило гласит, что из истинности двух дизъюнкций, одна
из которых содержит дизъюнкт, а другая – его отрицание,
следует (выводима) формула, которая является дизъюнкцией
исходных формул без упомянутого дизъюнкта и его отрицания.
Резолюция записывалась в следующем виде:
,
или эквивалентно
,
.
В логике предикатов первого порядка она выглядит так
же. Формулы
,,
в ней являются формулами этой логики.
Введем по аналогии с обощенным правилом модус поненс
обобщенное правило резолюции, или обобщённую резолюцию:
)()()()()(
)()(
m
m
mi
i
i
i
i
ii
i
i
xxxxx
1
1
1
1
1
1
1
1
1
,
)()()()()(
)()(
n
n
nj
j
j
j
j
jj
j
j
yyyyy
1
1
1
1
1
1
1
1
1
,
,,(),( jiji
ji
Унификация
)))(),((
j
j
ji
i
i
yx
Подстановка
)()()()(
)()(
1
1
1
1
1
1
1
1
1 i
i
i
i
i
ii
i
i
xxxx
)(
m
m
m
x
)()()()(
)()(
1
1
1
1
1
1
1
1
1 j
j
j
j
j
jj
j
j
yyyy
)(
n
n
n
y
.
Здесь
),(
i
i
i
x
mi )(11
обозначается литерал, такой, что
),()(
iii
i
i
xx
при
1i
и
)()(
i
i
ii
i
i
xx
при
0i
. Аналогичный
смысл имеет символ
j
в литерале
),(
j
j
j
y
nj )(11
.
Подстановка
))(( f
означает формулу, которая получает из
формулы
f
в результате подстановки
во все её атомы.
Суть обобщенного правила модус поненс можно ыразить
следующим образом. Если существует истинная формула
)()()()()(
)()(
m
m
mi
i
i
i
i
ii
i
i
xxxxx
1
1
1
1
1
1
1
1
1
,
которая является дизъюнкцией литералов
),(
i
i
i
x
mi )(11
, и
истинная формула
)()()()()(
)()(
n
n
nj
j
j
j
j
jj
j
j
yyyyy
1
1
1
1
1
1
1
1
1
,
которая также является дизъюнкцией литералов
),(
j
j
j
y
nj )(11
, и в этих формулах предикатные символы литералов
)(
i
i
i
x
и
)(
j
j
j
y
одинаковы
)(
ji
,
ji
, и для атомов
)(
i
i
i
x
и
)(
j
j
j
y
существует унификация
, которая делает их (записывается
как Унификация
),((
ii
x
)))(
jj
y
, то можно вывести истинную
формулу, которая получается в результате подстановки
в
дизъюнцию исходных формул после удаления в них литералов
)(
i
i
i
x
и
)(
j
j
j
y
. Выведенную таким образом истинную формулу
называют резольвентой. Так же как и в случае резолюции для
логики высказываний, обобщенную резолюцию можно выразить с
использованием импликации. Обратим внимание, что исходные
формулы в обобщенной резолюции и резольвента являются
дизъюнкцией литералов. Обычно такие формулы называют
клаузальными формами, или клаузами. Таким образом,
использование резолюции для вывода требует клаузальной
формы представления знаний. Это, в свою очередь, означает,
что база знаний, вывод для которой осуществляется на основе
обобщенной резолюции, должна представлять собой
совокупность клауз, понимаемых в целом как формула, которая
является конъюнкцией клауз. Формулы такого типа обычно
называют конъюнктивными нормальными формулами.
Прямой вывод на основе резолюции. Вернёмся теперь к
примеру с кубиками и повторим прямой вывод той же целевой
формулы, но уже используя обобщенную резолюцию. Заметим,
что формулы (11.1), (11.4) уже являются клаузами. остальные
формулы с помощью простейших преобразований на оснвое
закона
легко преобразуются в клаузы. В
результате вместо (11.5)-(11.10) получим следующие формулы.
Формулы, которые определяют условия выполнения
действий.
).( 113
на
),( yx
свободен
)(x
переместить
x(
, Стол
)
,
).( 213
на
x(
, Стол
)
свободен
)(x
свободен
)(z
переместить
),( zx
.
Формулы, определяющие условия переходов состояний
среды:
).( 313
на
),( yx
свободен
)(x
переместить
x(
,Стол
)
на
x(
, Стол
)
,
).( 413
на
),( yx
свободен
)(x
переместить
x(
,Стол
)
свободен
)(y
,
).( 513
на
),( yx
свободен
)(x
свободен
)(z
переместить
),( zx
на
),( zx
,
).( 613
на
),( yx
свободен
)(x
свободен
)(z
переместить
),( zx
свободен
)(y
.
Целевая формула. Целевая формула в соответствии с рис.
11.1 является конъюнкцией литералов и при прямом выводе,
как и в случае использования обобщенного правила модус
94
поненс, будет выводится для каждого литерала, входящего в
её состав, раздельно
).( 713
на (A,B) на (B, Стол) на (С, Стол) на (D, Стол) .
Вывод. Используя унифицированные клаузы (11.1), (13.1),
которые после унификации првращаются в клаузы (13.8),
(13.9) получаем резольвенту (13.10):
).( 813
на (A,С),
).( 913
на (A,С) свободен (A) переместить (A, Стол),
).( 1013
свободен (A) переместить (A, Стол).
Используя клаузы (11.3), (13.10), получаем резольвенту
).( 1113
переместить (A, Стол).
Используя эту резольвенту и унифицированную клаузу
(13.4), которая после унификации превратилась в клаузу
(13.12), получаем резольвенту (13.13):
).( 1213
на (A,y) свободен (A) переместить (A, Стол)
свободен (y),
).( 1313
на (A,y) свободен (A) свободен (y).
Затем, используя клаузы (11.1), (11.3) и
унифицированный резольвент (13.13), получаем резольвенту
).( 1413
свободен (C).
Аналогично можем получить следующие резольвенты:
).( 1513
на (A, Стол),
).( 1613
переместить (D, Стол),
).( 1713
свободен (B),
).( 1813
на (D, Стол).
Итак, кубики A и D могут быть перемещены на стол, в
результате чего кубики B и C окажутся свободными. После
этого, используя клаузы (11.5), (11.6), (13.15) и клаузу
(13.2), которая после унификации превращается в клаузу
(13.19), получаем резольвенту (13.20)
).( 1913
на (A, Стол) свободен (A) свободен (B)
переместить (A,B),
).( 2013
переместить (A,B).
95
Наконец, воспользовавшись клаузами (11.5), (11.6),
(13.15), (13.20) и клаузой (13.5), которая после унификации
превращается в клаузу (13.21), получим резольвенту (13.22):
).( 2113
на (A, Стол) свободен (A) свободен (B)
переместить (A,B) на (A,B),
).( 2213
на (A,B).
Таким образом, снова имеем истинные атомы на (A,B), на
(B, Стол), на (D, Стол). Согласно правилу введения конъюнкции,
вновь делаем заключение об истинности целевой формулы
на (A,B) на (B, Стол) на (С, Стол) на (D, Стол) .
На этом прямой вывод с использованием обобщенного
правила резолюции завершён.
Достоинством использования обобщенного правила
резолюции для прямого вывода является способность выводить
большое количество формул по сравнению с выводом на основе
обобщенного правила модус поненс. В процессе вывода база
знаний по-прежнему разрастается за счёт занесения в неё
вновь выводимых формул. Некоторые из этих формул могут
оказаться ненужными для вывода целевой формулы.
Как уже отмечалось, Робинсон предложил использовать
обобщенную резолюцию для создания стратегии вывода, в
основе которой лежит опровержение, или доведение до
противоречия. Идея этой стратегии вывода состоит в
следующем. Предположим необходимо вывести истинность
целевой формулы
. делается опровержение этой формулы,
т.е. предполагается истинным её отрицание
. Эта формула,
которая является отрицанием целевой, заносится в базу
знаний. После этого, если, начиная обратный вывод с формулы
, удастся установить противоречие, т.е. вывести пару
литералов
и
, то считается, что сделанное
предположение об истинности отрицания целевой формулы
ошибочно (опровергнуто) и делается заключение об истинности
целевой формулы
. Если в результате рассмотрения всех
возможных путей вывода такого противоречия установить не
удаётся, то считается, что целевая формула является ложной.
Рассмотрим стратегию обратного вывода на основе
опровержения для примера с кубиками.
Обратный вывод на основе опровержения и обобщенной
резолюции. Как уже отмечалось, вывод истинности целевой
формулы может лсуществляться по очереди литерал за
литералом. Поэтому рассмотрим его только для одно литерала
на (A,B) целевой формулы (13.7). Опровержение литерала на
96
(A,B) является литерал на (A,B). Обратный вывод
начинается именно с этого литерала. для того чтобы можно
было детально проследить процесс вывода, будем записывать
на каждом шаге вывода с помощью обобщенной резолюции три
формулы – две исходные и резольвенту, нумеруя по ходу
вывода получаемые резольвенты, а также указывая для каждого
шага используемые подстановки и подчёркивая те литералы,
которые в резольвенту не попадают:
).( 2313
на ( A , B ) ;
).( 2413
на (A, Стол) свободен (A) свободен (B)
переместить (A,B) на ( A , B ) ;
).( 2513
на (A, Стол) свободен (A) свободен (B)
переместить (A,B) ;
).( 2613
на (A, Стол) свободен (A) свободен (B)
переместить ( A , B ) ;
).( 2713
на (A, Стол) свободен (A) свободен (B)
переместить (A,B) ;
).( 2813
на (A, Стол) свободен (A) свободен (B);
).( 2913
на (A, Стол) свободен ( A ) свободен (B);
).( 3013
свободен ( A ) ;
).( 3113
на (A, Стол) свободен ( B ) ;
).( 3213
на ( A , Стол ) свободен (B) ;
).( 3313
на (A, y) свободен (A) переместить (A, Стол)
на ( A , Стол ) ;
).( 3413
на (A, y) свободен (A) переместить (A, Стол)
свободен (B);
).( 3513
на (A, y) свободен ( A ) переместить (A, Стол)
свободен (B);
).( 3613
свободен ( A ) ;
).( 3713
на (A, y) переместить (A, Стол) свободен (B);
).( 3813
на (D,B) свободен (D) переместить ( D , Стол )
свободен (B);
).( 3913
на (D,B) свободен (D) переместить ( D , Стол ) ;
97
).( 4013
на (D,B) свободен (D) свободен (B) ;
).( 4113
на (D,B) свободен ( D ) свободен (B) ;
).( 4213
свободен ( D ) ;
).( 4313
на (D,B) свободен (B) ;
).( 4413
на (D,B) свободен (B) ;
).( 4513
на (D,B);
).( 4613
свободен (B) ;
).( 4713
свободен (B) ;
).( 4813
свободен (B) ;
).( 4913
Nil.
Преобразование произвольной формулы логики предикатов
первого порядка в клаузальную форму. Применение обощенного
правила резолюции требует представления формул в каузальной
форме. Здесь мы покажем, с помощью каких эквивалентных
преобразования любая произвольная формула логики предикатов
первого порядка может быть преобразована в каузальную
форму. Процедуру преобразования представим в виде отдельных
шагов.
Исключение импликаций. Из логики высказываний известно,
что
. Поэтому на первом шаге с помощью этой
формулы исключаем все импликации.
Перемещение знака отрицания () непосредственно к
атомам. В клаузах отрицание допустимо только перед атомами.
Поэтому используя перечисленные ниже законы Де Моргана,
эквивалентности кванторов и двойного отрицания, перемещаем
знак отрицания непосредственно к атомам:
)(
,
)(
,
)()( xxxx
,
)()( xxxx
,
.
Переименование переменных. Во всех формулах, в которых
встречаются кванторы, использующие одни и те же связанные
переменные, как, например, в формуле
)()( xxxx
,
переименовываем связанные переменные таким образом, чтобы
они были индивидуальными для каждого квантора. Например,
для нашего примера это может быть использование переменной
98
y
вместо переменной
x
для квантора существования. В
результате получится формула
)()( yyxx
.
Перемещение кванторов влево. После предыдущего шага, в
результате которого каждый квантор использует свои
связанные переменные, обозначения которых не совпадают с
переменными других кванторов все кванторы перемещаем влево.
Так, например, простая
)(xx
после перемещения
квантора влево примет вид
)(xx
.
Сколемизация. Сколемизацией называется специфический
приём удаления кванторов существования. В простейшем случае
– это замена формулы
)(yy
на формулу
)(A
, где
A
является константой, которая ранее не встречалась. В общем
случае, когда переменная, которая связывается квантором
существования. встречается в каком-либо литерале вместе с
переменными, связанными квантором общности, приходится,
чтобы избавиться от квантора общности, вводить специальную
функцию, которая зависит от переменных, связанных квантором
обшности, вместо переменной, связанной квантром
существования.
Так, если имеем формулу
)))(()( x,yyyxx (
,
то здесь литерал
)(y
может означать, например, наличие
некоторого свойства, именуемого предикатным символом
, у
объекта, именуемого переменной
y
, а атом
),( yx
задаёт
отношение между объектами
yx,
. Объект, который обозначен
переменной
y
, определяется в этом случае значением
переменной
x
и может быть заменен на ранее не
встречавшуюся функцию
)(xF
, которая обычно называют
функцией Сколема. После такой замены квантор сущестования
может быть удален, а формула приобретает вид
))())(()( xx,FxFxx (
.
Распределение конъюнкций относительной дизъюнкций. Это
распределение осуществляется на основе использования
дистрибутивного закона
)()()(
.
Перемещение скобок к концу и началу. На этом шаге
формулы со скобками типа
)(
или
)(
приводятся
соответственно к виду
)(
или
)(
. После этого
шага исходная формула преобразуется в нормальную
конъюнктивную форму, которая является конъюнкцией
дизъюнкцией литаралов. Каждая дизъюнкция литералов является
клаузой.
99
14.АВТОМАТ И СРЕДА
Ранее было введено понятие формального языка логики
высказываний, который используется для представления знаний
о среде. С помощью этого языка осуществлялось решение задач
нахождения последовательностей действий, которые ведут в
целевые состояния. Таким образом, агент, который решают ту
или иную задачу, фактически чаще всего имеет дело не с
самой средой, а с некоторым её представлением или описанием
на каком-либо языке. Поэтому он должен знать, как этот язык
устроен, для этого, чтобы понимать описание, составленное
на нём. Далее будут рассмотрены вопрсоы описания языков с
помощью формальных грамматик и использование такого
описания агентом.
Стратегия поиска целевых состояний и ведущих в них
последовательностей действий примера со средой кота
состояла в рассмотрении всех возможных состояний и
переходов из каждого состояния при выполнении каждого
действия. Для решения задачи поиска золота в примере для
среды чудовища применялась похожая стратегия, но с
использованием не состояний, а интервалов. Отмечалось, что
стратегии подобного типа неэкономны по числу шагов,
используемых для поиска цели.
Описанию различных стратегий поиска будет посвящен
соответствующий материал далее. Сложность поиска зависит
как от объёма описания знаний о среде на том или ином
языке, так и от стратегии поиска. Если описание избыточно,
то часть времени поиска может расходоваться впустую на
анлиз избыточной информации. Ниже будет показано также, как
может быть сокращен объём описания на языке в задачах
поиска целевых состояний.
Конечным инициальным детерминированным автоматом
называют объект, который определяется следующими шестьюми
понятиями.
Входной алфавит
}.,,,{
m
aaaA
21
Внутренний алфавит (множество состояний автомата)
}.,,,{
n
bbbB
21
Выходной алфавит
}.,,,{
p
сссС
21
Функция перехода
f
:
CBA
, записываемая так же, как
ji
bbaf ),(
, где
BbbAa
ji
,,
.
Функция выходов
:
CB
, записываемая так же, как
ii
cb )(
, где
CcBb
ii
,
.