A,a®b)/b

Пример. Пусть имеются следующие истинные высказывания:
1. Если самолет проверен и заправлен, то он готов к вылету.
2. Если самолет готов к вылету и дано разрешение на взлет, то он либо взлетел, либо находится на взлётной полосе.
3. Если самолет взлетел, то он выполняет рейс.
4. Самолет ЯК-42 проверен и заправлен.
5. Самолет ТУ-134 проверен.
6. Самолет ИЛ-62 заправлен.
7, Самолету ЯК-42 дано разрешение на вылет.
8. Самолет ЯК-42 не находится на взлетной полосе.
Требуется найти, какой из самолетов в момент времени Т выполняет рейс.
Проведем анализ данных высказываний. Высказывания 1, 2, 3 являются сложными и построены с использованием логических связок ®(импликация), L(И). Во всех элементарных высказываниях, из которых построены предложения 1, 2, 3, субъектом является понятие «самолет»; предикатами выступают сказуемые, описывающие свойства всех объектов, принадлежащих классу «самолет». Высказывания 4-8 являются фактами, ис-тинными на момент времени Т. Они являются элементарными высказываниями, описы-вающими свойства конкретных объектов предметной области.
Для формального описания задачи введем следующие одноместные предикаты:
ПРОВЕРЕН(Х) — самолет X проверен;
ЗАПРАВЛЕН(Х) — самолет X заправлен;
ГОТОВ(Х) — самолет X готов к вылету;
ДАНО_РАЗР(Х) — самолету X дано разрешение на вылет; .
ВЗЛЕТЕЛ(Х) - самолет X взлетел;
НАХ_ВЗП(Х) — самолет X находится на взлетной полосе;
НЕ_НАХ_ВЗП(Х) — самолет X не находится на взлетной полосе;
ВЫП_РЕЙС(Х) — самолет X выполняет рейс.
Тогда исходное описание на языке логики предикатов будет иметь вид:
1. "Х(ПРОВЕРЕН(Х)LЗАПРАВЛЕН(Х)®ГОТОВ(Х))
2. "Х(ГОТОВ(Х}LДАНО_РАЗР(Х)UHE_НАХ_ВЗП(Х)®ВЗЛЕТЕЛ(Х))
3. "Х(ГОТОВ(Х)LДАНО_РАЗР(Х)UO ВЗЛЕТЕЛ(Х)®НАХ_ВЗП(Х))
4. "Х(ВЗЛЕТЕЛ(Х)®ВЫП_РЕЙС(Х))
5. ПРОВЕРЕН(ЯК-42)
6. ЗАПРАВЛЕН(ЯК-42)
7. ПРОВЕРЕН(ТУ-134)
8. ЗАПРАВЛЕН(ИЛ-62)
9. ДАНО_РАЗР(ЯК-42)
Ю.НЕ_НАХ_ВЗП(ЯК-42)
Предложения 1-4, хотя и содержат переменную, являются высказываниями — пере-менная X связана квантором общности V. В дальнейшем квантор писать не будем, так как он присутствует во всех предложениях.
Чтобы найти, какой из самолетов в момент времени Т выполняет рейс, подготовим запрос вида:
М ÞВЫП_РЕЙС(Z),
где М — множество предложений 1-10.
Вывод запроса можно представить следующей последовательностью шагов.
1 шаг.
Применив к предложению 1 подстановку Х=ЯК-42, получим заключение
ПРОВЕРЕН(ЯК-42)LЗАПРАВЛЕН(ЯК-42)®ГОТОВ(ЯК-42).
2 шаг.
Первая посылка: объединив предложения 5 и 6, получим
ПРОВЕРЕН(ЯК-42)LЗАПРАВЛЕН(ЯК-42).
Вторая посылка: заключение шага 1:
ПРОВЕРЕН(ЯК-42)LЗАПРАВЛЕН(ЯК-42)®ГОТОВ(ЯК-42).
Применив правило Modus Ponens
(a,a®b)/b

для a= ПРОВЕРЕН(ЯК-42) LЗАПРАВЛЕН(ЯК-42) и (b= ГОТОВ(ЯК-42), получим следующее заключение: ГОТОВ(ЯК-42).
3 шаг.
Первая посылка: объединив заключение шага 2, предложения 9 и 10, получим:
ГОТОВ(ЯК-42) LДАНО_РАЗР(ЯК-42) LНЕ_ НАХ_ВЗП(ЯК-42).
Вторая посылка: применив к правилу 2 подстановку Х=ЯК-42, получим
ГОТОВ(ЯК-42) LДАНО_РАЗР(ЯК-42)LНЕ_НАХ_ВЗП(ЯК-42) ®
ВЗЛЕТЕЛ(ЯК-42)
Применив правило Modus Ponens, получим заключение ВЗЛЕТЕЛ(ЯК-42).
4 шаг
Первая посылка: заключение шага 3 - ВЗЛЕТЕЛ(ЯК-42).
Вторая посылка: применив к правилу 4 подстановку Х=ЯК-42, получим
ВЗЛЕТЕЛ(ЯК-42) ®ВЫП_РЕЙС(ЯК-42).
Применив правило Modus Ponens, получим заключение ВЫП_РЕЙС(ЯК-42).
Таким образом, в момент времени Т рейс выполняет самолет ЯК-42. Остальные подстановки, например Х=ИЛ-62, приводят к тупиковым ситуациям. Логический вывод выполнялся нами в прямом направлении, при этом в процессе вывода трижды использовалось правило заключения.

 

Формальные модели представления знаний.

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

Логические выражения, построенные в данном языке, могут быть истинными или ложными. Некоторые из этих выражений, являющиеся всегда истинными. Объявляются аксиомами (или постулатами). Они составляют ту базовую систему посылок, исходя из которой и пользуясь определенными правилами вывода, можно получить заключения в виде новых выражений, также являющихся истинными.

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

Формальная теория должна, таким образом, удовлетворять следующему определению:

всякая формальная теория F = (A, V, W, R), определяющая некоторую аксиоматическую систему, характеризуется:

наличием алфавита (словаря), A,

множеством синтаксических правил, V,

множеством аксиом, лежащих в основе теории, W,

множеством правил вывода, R.

Исчисление высказываний (ИВ) и исчисление предикатов (ИП) являются классическими примерами аксиоматических систем. Эти ФС хорошо исследованы и имеют прекрасно разработанные модели логического вывода - главной метапроцедуры в интеллектуальных системах. Поэтому все, что может и гарантирует каждая из этих систем, гарантируется и для прикладных ФС как моделей конкретных предметных областей. В частности, это гарантии непротиворечивости вывода, алгоритмической разрешимости (для исчисления высказываний) и полуразрешимости (для исчислений предикатов первого порядка).

ФС имеют и недостатки, которые заставляют искать иные формы представления. Главный недостаток - это "закрытость" ФС, их негибкость. Модификация и расширение здесь всегда связаны с перестройкой всей ФС, что для практических систем сложно и трудоемко. В них очень сложно учитывать происходящие изменения. Поэтому ФС как модели представления знаний используются в тех предметных областях, которые хорошо локализуются и мало зависят от внешних факторов.