Для представления математического знания в математической логике пользуются логическими формализмами — исчислением высказываний и исчислением предикатов. Эти формализмы имеют ясную формальную семантику и для них разработаны механизмы вывода. Поэтому исчисление предикатов было первым логическим языком, который применяли для формального описания предметных областей, связанных с решением прикладных задач.
Логические модели представления знаний реализуются средствами логики предикатов.
Предикатом называется функция, принимающая два значения (истина или ложь) и предназначенная для выражения свойств объектов или связей между ними. Выражение, в котором утверждается или отрицается наличие каких-либо свойств у объекта, называется высказыванием. Константы служат для именования объектов предметной области. Логические предложения или высказывания образуют атомарные формулы. Интерпретация предиката — это множество всех допустимых связываний переменных с константами. Связывание представляет собой подстановку констант вместо переменных. Предикат считается общезначимым, если он истинен во всех возможных интерпретациях. Говорят, что высказывание логически следует из заданных посылок, если оно истинно всегда, когда истинны посылки.
Описания предметных областей, выполненные в логических языках, называются логическими моделями.
Пример.
ДАТЬ (МИХАИЛ, ВЛАДИМИРУ, КНИГУ);
($x) (ЭЛЕМЕНТ (x, СОБЫТИЕ-ДАТЬ) ? ИСТОЧНИК (x, МИХАИЛ) ? АДРЕСАТ ? (x, ВЛАДИМИР) ОБЪЕКТ(x, КНИГА).
Здесь описаны два способа записи одного факта: «Михаил дал книгу Владимиру».
Логический вывод осуществляется с помощью силлогизма (если из A следует B, а из B следует C, то из A следует C).
В общем случае в основе логических моделей лежит понятие формальной теории, задаваемой четверкой:
S = <B, F, A< R>,
где B — счетное множество базовых символов (алфавит) теории S;
F — подмножество выражений теории S, называемые формулами теории (под выражениями понимаются конечные последовательности базовых символов теории S);
A — выделенное множество формул, называемые аксиомами теории S, то есть множество априорных формул;
R — конечное множество отношений {r1, …, rn} между формулами, называемые правилами вывода.
Преимущество логических моделей представления знаний заключается в возможности непосредственно запрограммировать механизм вывода синтаксически правильных высказываний. Примером такого механизма служит, в частности процедура вывода, построенная на основе метода резолюций.
Покажем метод резолюций.
В методе используется несколько понятий и теорем.
Понятие тавтологии, логической формулы, значением которой будет «истина» при любых значениях входящих в них атомов. Обозначается ?, читается как «общезначимо» или «всегда истинно».
Теорема 1. А?В тогда и только тогда, когда ?А
В.
Теорема 2. А1, А2, ..., Аn ? В тогда и только тогда, когда ? (A1?A2?A3?…?An) В.
Символ ? читается как «верно, что» или «можно вывести».
В основе метода лежит доказательство тавтологии
? (X?A)?(Y??A)?(X?Y) .
Теоремы 1 и 2 позволяют записать это правило в следующем виде:
(X?A), (Y??A) ? (X?Y),
что дает основания утверждать: из посылок 
и 
можно вывести 
.
В процессе логического вывода с применением правила резолюции выполняются следующие шаги.
1. Устраняются операции эквивалентности и импликации:
;
.
2. Операция отрицания продвигается внутрь формул с помощью законов де Моргана:
3. Логические формулы приводятся к дизъюнктивной форме: 
.
Правило резолюции содержит в левой части конъюнкцию дизъюнктов, поэтому приведение посылок, используемых для доказательства, к виду, представляющему собой конъюнкции дизъюнктов, является необходимым этапом практически любого алгоритма, реализующего логический вывод на базе метода резолюции. Метод резолюции легко программируется, это одно из важнейших его достоинств.
Предположим, нужно доказать, что если истинны соотношения 
и 
, то можно вывести формулу 
. Для этого нужно выполнить следующие шаги.
1.Приведение посылок к дизъюнктивной форме:
, 
, 
.
2.Построение отрицания выводимого заключения 
. Полученная конъюнкция справедлива, когда 
и 
одновременно истинны.
3.Применение правила резолюции:
;
;
;
(противоречие или «пустой дизъюнкт»).
Итак, предположив ложность выводимого заключения, получаем противоречие, следовательно, выводимое заключение является истинным, т.е. , выводимо из исходных посылок.
Именно правило резолюции послужило базой для создания языка логического программирования PROLOG. По сути дела, интерпретатор языка PROLOG самостоятельно реализует вывод, подобный вышеописанному, формируя ответ на вопрос пользователя, обращенный к базе знаний.
В логике предикатов для применения правила резолюции предстоит осуществить более сложную унификацию логических формул в целях их приведения к системе дизъюнктов. Это связано с наличием дополнительных элементов синтаксиса, в основном кванторов, переменных, предикатов и функций.
Алгоритм унификации предикатных логических формул включает следующие шаги.
- Исключение операций эквивалентности.
- Исключение операций импликации.
- Внесение операций отрицания внутрь формул.
- Исключение кванторов существования. Это может произойти на шаге 3 вследствие применения законов де Моргана, а именно; в результате отрицания
меняется на 
, но при этом может произойти и обратная замена. Тогда для исключения поступают следующим образом; все вхождения некоторой переменной, связанной квантором существования, например 
, заменяются в формуле на новую константу, например а. Эта константа представляет собой некоторое (неизвестное) значение переменной X, для которого утверждение, записанное данной формулой, истинно. При этом важно то, что на все места, где присутствует X, будет подставлено одно и то же значение а, пусть оно и является неизвестным в данный момент. Такие константы называются сколемовскими, а операция — сколемизацией (по имени известного математика Сколема). - Кванторы общности выносятся на первые места в формулах. Это также не всегда является простой операцией, иногда при этом приходится делать переименование переменных.
- Раскрытие конъюнкций, попавших внутрь дизъюнкций.
После выполнения всех шагов описанного алгоритма унификации можно применять правило резолюции, Обычно при этом осуществляется отрицание выводимого заключения, и алгоритм вывода можно кратко описать следующим образом: Если задано несколько аксиом (теория Тh) и предстоит сделать заключение о том, выводима ли некоторая формула Р из аксиом теории Тh, строится отрицание Р и добавляется к Тh, при этом получают новую теорию Тh1. После приведения 
и аксиом теории к системе дизъюнктов можно построить конъюнкцию и аксиом теории Тh. При этом существует возможность выводить из исходных дизъюнктов дизъюнкты - следствия. Если Р выводимо из аксиом теории Тh, то в процессе вывода можно получить некоторый дизъюнкт Q, состоящий из одной литеры, и противоположный ему дизъюнкт 
. Это противоречие свидетельствует о том, что Р выводимо из аксиом Тh. Вообще говоря, существует множество стратегий доказательства, нами рассмотрена лишь одна из возможных — нисходящая.
Пример: представим средствами логики предикатов следующий текст:
«Если студент умеет хорошо программировать, то он может стать специалистом в области прикладной информатики».
«Если студент хорошо сдал экзамен по информационным системам, значит, он умеет хорошо программировать».
Представим этот текст средствами логики предикатов первого порядка. Введем обозначения: X — переменная для обозначения студента; хорошо — константа, соответствующая уровню квалификации; Р(Х) — предикат, выражающий возможность субъекта X стать специалистом по прикладной информатике; Q(Х, хорошо) — предикат, обозначающий умение субъекта X программировать с оценкой хорошо; R(Х, хорошо) — предикат, задающий связь студента X с экзаменационной оценкой по информационным системам.
Теперь построим множество правильно построенных формул:
Q(Х, хорошо)
.
R(Х, хорошо)Q(Х, хорошо).
Дополним полученную теорию конкретным фактом
R(иванов, хорошо).
Выполним логический вывод с применением правила резолюции, чтобы установить, является ли формула Р(иванов) следствием вышеприведенной теории. Другими словами, можно ли вывести из этой теории факт, что студент Иванов станет специалистом в прикладной информатике, если он хорошо сдал экзамен по информационным системам.
Доказательство
1. Выполним преобразование исходных формул теории в целях приведения к дизъюнктивной форме:
(Х,хорошо)
Р(Х);
(Х,хорошо)
(Х,хорошо);
R(иванов, хорошо).
2. Добавим к имеющимся аксиомам отрицание выводимого заключения
(иванов).
3. Построим конъюнкцию дизъюнктов
(Х,хорошо)Р(Х)??P(иванов, хорошо)??Q(иванов, хорошо), заменяя переменную X на константу иванов.
Результат применения правила резолюции называют резольвентой. В данном случае резольвентой является (иванов).
4. Построим конъюнкцию дизъюнктов с использованием резольвенты, полученной на шаге 3:
(Х, хорошо)(Х, хорошо)
(иванов, хорошо) 
(иванов, хорошо).
5. Запишем конъюнкцию полученной резольвенты с последним дизъюнктом теории:
(иванов, хорошо)
(иванов, хорошо) 
(противоречие).
Следовательно, факт Р(иванов) выводим из аксиом данной теории.
Для определения порядка применения аксиом в процессе вывода существуют следующие эвристические правила:
- На первом шаге вывода используется отрицание выводимого заключения.
- В каждом последующем шаге вывода участвует резольвента, полученная на предыдущем шаге.
Однако с помощью правил, задающих синтаксис языка, нельзя установить истинность или ложность того или иного высказывания. Это распространяется на все языки. Высказывание может быть построено синтаксически правильно, но оказаться совершенно бессмысленным. Высокая степень единообразия также влечет за собой еще один недостаток логических моделей — сложность использования при доказательстве эвристик, отражающих специфику конкретной предметной проблемы. К другим недостаткам формальных систем следует отнести их монотонность, отсутствие средств для структурирования используемых элементов и недопустимость противоречий. Дальнейшее развитие баз знаний пошло пути работ в области индуктивных логик, логик «здравого смысла», логик веры и других логических схем, мало что имеющих общего с классической математической логикой.