Эти модели на рис. 7.4, аиб обозначены соответственно как а1 и а2. Проанализировав все возможные ситуации, мы обнаружили следующее: в каждой модели, в которой база знаний является истинной, высказывание oci также является истинным. Поэтомув квадрате [1,2] нет ямы. Кроме того, можно убедиться в следующем: в некоторых моделях, в которых база знаний является истинной, высказывание a2 ложно. Поэтомуагент не может прийти к заключению, что в квадрате [2,2] нет ямы. (К тому же он не может сделать и вывод, что в квадрате [2,2] есть яма.)

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

Чтобы лучше понять, что такое логическое следствие и логический вывод, можно представить себе, что множество всех логических заключений, полученных из базы данных, — это стог сена, а высказывание а — это иголка. Логическое следствие напоминает утверждение о том, что в стоге сена есть иголка, а логический вывод можно сравнить с ее поиском. Это различие между понятиями логического следствия и логического вывода отражено и в формальных обозначениях: если некоторый алгоритм логического вывода i позволяет вывести логическим путем высказывание а из базы знаний КB, то можно записать следующее:

Эта формула читается так: "высказывание а получено путем логического вывода из базы знаний КБ с помощью алгоритма i" или "алгоритм i позволяет вывести логическим путем высказывание а из базы знаний КБ".