24. Модель представления знаний, основанная на исчислениях высказываний.

Логические исчисления могут быть представлены как формальные системы в виде четвёрки:

M = <T,P,A,F>,

Где T – это множество базовых элементов (например, имена высказываний, буквы некоторого алфавита, клетки шахматной доски и т.п.);

P – множество синтаксических правил, на основе которых из Т строятся правильно построенные формулы;

A – множество правильно построенных формул, элементы которого называются аксиомами;

F – правила вывода, которые из множества А позволяют получить новые правильно построенные формулы

Для множество Т в (M = <T,P,A,F>) существует некоторые способ определения принадлежности или непринадлежности произвольного элемента к этому множеству. Процедура такой проверки П(Т) может быть любой, но за конечно число шагов, она должна давать положительный или отрицательный ответ:

Аналогично для множества Р декларируется существование процедуры П(Р), с помощью которой за конечное число шагов можно ответить на вопрос, является ли совокупность Х синтаксически правильной, а для множества А – существование процедуры П(А), с помощью которой для любой синтаксически правильной совокупности можно получить ответ на вопрос о принадлежности её к множеству А.

Согласно синтаксическим правилам исчисления высказываний:

• Всякое элементарное высказывание является правильной формулой;

• Если α и β являются правильными формулами, то правильными формулами являются также:

• Других правильных формул в исчислении высказываний нет

Правила вывода в исчислении высказываний – это правила вида:

“из формул выводима формула G”:

Формулы называются посылками вывода, а G – заключением вывода.

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

Наиболее часто в качестве множества аксиом используются абсолютные аксиомы Гильберта-Аккермана:

Эта система аксиом является полной.

Процедура, которая из заданной группы выражений выводит отличное от них некоторое другое выражение, называется процедурой (механизмом) вывода. Правила вывода, которые из известных выражений выводят некоторое новое выражение, называется в исчислении высказываний правилами дедуктивного вывода.

Обычно используют 2 правила вывода:

• Правило подстановки;

• Правило заключения (Modus Ponens).

Правило подстановки формулируется следующим образом:

“из формулы A(S), содержащей букву S, выводима любая формула А(G), получающаяся заменой всех вхождений S в формуле A на произвольную(на одинаковую для всех вхождений S) формулу G.”

Так, если во вторую аксиому Гильбертавместоα подставить любую формулу, например (β & γ), то формула останется тождественно истинной.

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

Правило заключения (Modus Ponens) формулируется следующим образом:

“Если S и S ->B являются истинными формулами, то формула B тоже истинна”. Формально это правило имеет вид: