Высказывание – предложение, смысл которого можно оценить как «истинно» или «ложно». Логическая модель является формальной моделью представления знаний.

P: все люди смертны
Q: Сократ - человек
R: Сократ смертен
(P ^ Q) -> R

Предикат – логическая функция.
<константа> ::= <ид1>
<переменная> ::= <ид2>
<функция> ::= <ид3>
<предикат> ::= <ид4>
<терм> ::= <константа>|<переменная>|функция(<список термов>)
<список термов> ::= <терм>|<терм>, <список термов>
<атом> ::= <предикат>|<предикат>(<список термов>)
<литера> ::= <атом>|¬<атом>
<оператор> ::= < ^ >|< v >|< <=> >|< → >
<список переменных> ::= <переменная>|<переменная>, <список переменных>
<квантор> ::= <(∃<список переменных>)>|<(∀<список переменных>)>
<формула> ::= <литера>|¬ <формула>|<квантор>(<формула>)|(<формула>)<оператор>(<формула>)

---

Пример

Любит(X, Y);

1. (∀X)(∃Y) Любит(X, Y) Каждый X любит хотя бы одного Y
2. (∃Y)(∀X) Любит(X, Y) Сущ. Y, которого любят все Х
3. (∀X)(∀y) Любит(X0) Всеобщее человеколюбие
4. (∃X)(∀y) Любит(X0) Сущ. хотя бы 1 X кот. любит всех
5. (∀y)(∃X) Любит(X, Y) Каждого, кто-нибудь, да любит
6. (∃X)(∃y) Любит(X, Y)

---

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

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

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

Правила вывода

Наиболее известные правила дедукции:

• Modus Ponendo Ponens: [A → B, A] → [B]
• Modus Tollendo Tollens: [A → B, ¬B] → [¬A]
• Modus Ponendo Tollens: [¬(A ^ B), A] → [¬B]
• Modus Tollendo Ponens: [A v B, ¬A] → B
• Цепное правило: [A → B, B → C] → [A → C]

---

Пример

Обозначения
P := <Рост мировых цен на топливно-энергетические ресурсы>
Q := <Увеличивается поступление в бюджет>
R := <Рост производства>
S := <Укрепление рубля>
Высказывания

1. P → Q
2. (P or Q) → (S or R)
3. (P → Q) → ((P or Q) → (R or Q))
4. [1 & 3] → [(P or Q) → (R or Q)]
5. [4 & 2] → [(P or Q) → (R or S)]

---

Проблема доказательства в логике – нахождение истинного значения заключения B, если предполагается истинность исходных предпосылок A1, …, An. Существуют два способа решения проблемы доказательства:

• Семантический метод. Перечислить все атомы, входящие в формулы A1...Аn и B, составить таблицу истинности для всех возможных комбинаций значений этих атомов; затем осуществить просмотр полученной таблицы, дабы проверить, во всех ли её строках, где a1, …, an истинно, b также истинно. Этот метод универсален, но может оказаться очень трудоёмким.
• Синтаксический метод. Записываются посылки, затем к ним применяются правила вывода, стараясь получить из них другие истинные формулы. Из этих формул выводят последующие. До тех пор, пока не будет получено требуемое заключение (это не всегда возможно)

DEFs
Тавтология (теорема логики) — правильно построенная формула (ППФ), значение которой истинно при любых значениях входящих в нее атомов. Она называется также частным случаем исходной или результатом подставной.
Правило подстановки: если С(А) — тавтология, то С(В) — тоже тавтология.
Теория заданной области знаний – множество ППФ для некоторой предметной области.
Аксиома – каждое отдельно построенное утверждение.
Цель построения теорий – представление знаний наиболее экономичным способом. Если такую теорию удаётся построить, то все истинные факты из области интерпретации будут следствиями аксиом этой теории, то есть их можно будет вывести из множества правильно построенных формул. Ложные факты не будут следствиями теорий, т. е. их нельзя будет получать путем логического вывода из аксиом.

Непротиворечивая (синтаксически последовательная) теория – такая теория, что из аксиом нельзя вывести противоречие.
Полная теория – для любого утверждения можно определить его истинность или ложность.

---

Пример
Область интерпретации

А = <есть дом>
B = <дом может сгореть>
C = <есть жена>
D = <жена может уйти к другому>

Правила

• [¬A] → [¬B]
• [¬C] → [¬D] Данная теория является противоречивой

---

Алгоритм унификации предикатных логических формул

1. Исключение операций эквивалентности.
2. Исключение операций импликации.
3. Внесение операций отрицания внутрь формул.
4. Исключение кванторов существования. Это может про​изойти на шаге 3 вследствие применения законов де Моргана, а именно: в результате отрицания ∃ меняется на ∀, но при этом мо​жет произойти и обратная замена. Тогда для исключения ∃ посту​пают следующим образом: все вхождения некоторой перемен​ной, связанной квантором существования, например (∃X), заме​няются в формуле на новую константу, например а. Эта констан​та представляет собой некоторое (неизвестное) значение пере​менной X, для которого утверждение, записанное данной форму​лой, истинно. При этом важно то, что на все места, где присутст​вует X, будет подставлено одно и то же значение а, пусть оно и яв​ляется неизвестным в данный момент. Такие константы называ​ются сколемовскими, а операция — сколемизацией (по имени изве​стного математика Сколема).
5. Кванторы общности выносятся на первые места в форму​лах. Это также не всегда является простой операцией, иногда при этом приходится делать переименование переменных.
6. Раскрытие конъюнкций, попавших внутрь дизъюнкций, т.е. бескванторную часть формулы привести к конъюнктивной нормальной форме (КНФ).
   После выполнения всех шагов описанного алгоритма унифи​кации можно применять правило резолюции. Обычно при этом осуществляется отрицание выводимого заключения, и алгоритм вывода можно кратко описать следующим образом: Если задано несколько аксиом (теория Тh) и предстоит сделать заключение о том, выводима ли некоторая формула Р из аксиом теории Тh, строится отрицание Р и добавляется к Тh, при этом получают но​вую теорию Тh1. После приведения ¬P и аксиом теории к систе​ме дизъюнктов можно построить конъюнкцию ¬P и аксиом тео​рии Тh. При этом существует возможность выводить из исходных дизъюнктов дизъюнкты-следствия. Если Р выводимо из аксиом теории Тh, то в процессе вывода можно получить некоторый дизъюнкт Q, состоящий из одной литеры, и противоположный ему дизъюнкт ¬Q. Это противоречие свидетельствует о том, что Р выводимо из аксиом Тh. Вообще говоря, существует множество стратегий доказательства, нами рассмотрена лишь одна из воз​можных — нисходящая.

---

Пример. Представим средствами логики предикатов следую​щий текст:

«Если студент умеет хорошо программировать, то он может стать специалистом в области информационных технологий».

«Если студент хорошо сдал экзамен по технологии программирования, значит, он умеет хорошо программировать».

Представим этот текст средствами логики предикатов перво​го порядка. Введем обозначения: X — переменная для обозначе​ния студента; хорошо — константа, соответствующая уровню квалификации; Р(Х) — предикат, выражающий возможность субъекта X стать специалистом в области информационных технологий; Q(X, хорошо) — предикат, обозначающий умение субъекта X про​граммировать с оценкой хорошо; R(Х, хорошо) — предикат, задаю​щий связь студента X с экзаменационной оценкой по технологии программирования.

Теперь построим множество ППФ:

(∀Х)Q(Х, хорошо) → Р(Х)

(∀Х)R(Х, хорошо) → Q(Х, хорошо)

Дополним полученную теорию конкретным фактом R(Иванов, хорошо).

Выполним логический вывод с применением правила резо​люции, чтобы установить, является ли формула Р(Иванов) следст​вием вышеприведенной теории. Другими словами, можно ли вы​вести из этой теории факт, что студент Иванов станет специалис​том в области информационных технологий, если он хорошо сдал экзамен по технологии программирования.

Доказательство.

1. Выполним преобразование исходных формул теории в це​лях приведения к дизъюнктивной форме:

(∃Х) ¬Q(Х,хорошо) & Р(Х);

(∃Х) ¬R(Х,хорошо) v Q(Х,хорошо); 

R(иванов, хорошо).

2. Добавим к имеющимся аксиомам отрицание выводимого заключения

¬Р(иванов)

3. Построим конъюнкцию дизъюнктов

(∃Х) Q(Х, хорошо) v Р(Х) & Р(иванов) → ¬Q(иванов, хорошо),

заменяя переменную X на константу иванов.

Результат применения правила резолюции называют резольвентой. В данном случае резольвентой является Q(иванов).

4. Построим конъюнкцию дизъюнктов с использованием ре​зольвенты, полученной на шаге 3:

(∃Х) ¬R(Х, хорошо) v (Х, хорошо) & ¬Q(иванов, хорошо) → ¬R(иванов, хорошо)

5. Запишем конъюнкцию полученной резольвенты с послед​ним дизъюнктом теории:

¬R(иванов, хорошо) & R(иванов, хорошо) → F (противоречие). Следовательно, факт Р(иванов) выводим из аксиом данной теории.

---

Для определения порядка применения аксиом в процессе вы​вода существуют следующие эвристические правила:

1. На первом шаге вывода используется отрицание выводимо​го заключения.

2. В каждом последующем шаге вывода участвует резольвен​та, полученная на предыдущем шаге.

Программа ЛОГИК-ТЕОРЕТИК была предназначенная для автоматического доказательства теорем в исчислении высказываний. Пусть есть два утверждения: ƒ1 и ƒ2. Нужно доказать их тождественную истинность. Если для всех введём набор интерпретаций истинности входящих в них элементов, высказываемая истинность одинакова (?).

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

Было введено шесть типов различий:

1. Различное число членов f1 = A v AB; f2 = A v B
2. Различие в основной связке f1 = (AB) v (A ¬B); f2=(AvB) → A
3. Различие в наличии отрицания перед формулой
4. Различие в наличии отрицания перед подвыражением
5. Различие в расстановке скобок
6. Различие в порядке следования подвыражений.

• F1: A & B <=> B & A
• A v B <=> B v A
• F2: A → B <=> ¬B → ¬A