Основы построения и функционирования интеллектуальных информационных систем. Былкин В.Д - 37 стр.

вильные конструкции; А        - множество априорно-истинных конструкций,           называемых
аксиомами; Ф - семантические правила вывода, позволяющие расширить множество А за счет
других конструкций, которые в рамках данной формальной системы также считаются
истинными.    Способ   построения     формул    (множество   Р   )   определяет     конкретную
синтаксическую конструкцию формул или грамматику формул, которые представляют собой
правильно построенные последовательности символов конечного алфавита (множестве Т). В
отличие от этого множество Ф задает разрешенные правила вывода формул друг из друга.
Формальное доказательство определяется как конечная последовательность формул A1, A2, ... , Ar,
причем каждая формула Ai либо является аксиомой, либо выводима из предшествующих ей
формул с помощью одного из правил вывода. Любая формула t называется теоремой, если
существует доказательство, в котором она является последней, т.е. Ar = t. В частности, всякая
аксиома является теоремой. Если t есть теорема, то этот факт кратко обозначается так: |-t. Таким
образом, правила вывода (правила словообразования) позволяют определять, является ли данная
формула теоремой формальной системы.
В качестве примера рассмотрим следующую формальную систему:
1. Базовые элементы: "М", "Я". "У".
2. Синтаксические правила (формулы): любая последовательность символов алфавита.
3. Аксиомы: "МЯ".
4. Правила вывода
         правило 1:      «сЯ»          «сЯУ»;
         правило 2:      «Мс»          «Мсс»;
         правило 3:      «ЯЯЯ»         "У";
         правило 4:      «УУ»          « ».
Правило 1 применимо только, если последний символ теоремы, есть "Я". Например, из теоремы
"МЯУМЯ" можно вывести теорему "МЯУМЯУ. Отметим, что символ "с" не принадлежит
множеству Т (алфавиту) данной формальной системы, а просто играет роль некоего слова.
Правило 2 позволяет, например, из теоремы "МУЯ" вывести теорему "МУЯУЯ" при условии, что
"МУЯ" является теоремой. Правило 3 позволяет, например, сделать переход от теоремы
―МУЯЯЯУМ‖ к теореме "МУУУМ". Последнее правило 4 указывает; что всякая цепочка из двух
рядов стоящих символов "У" может быть просто удалена из теоремы, например, теорема




                                                37