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

3. РЕШЕНИЕ ЛОГИЧЕСКИХ ЗАДАЧ НА ОСНОВЕ ИСЧИСЛЕНИЯ
      Кардинальный сдвиг в анализе стандартных рассуждений произошел в тот период, когда
для создания логической теории был применен метод построения формальных систем с помощью
специальных символических языков. Были созданы две мощные формальные системы, которые
впервые позволили автоматизировать рассуждения, опирающиеся на схему дедуктивного вывода:
исчисления высказываний (ИВ) и исчисления предикатов (ИП).
      Под высказыванием будем понимать утверждение, относительно которого в любой
момент, можно сказать, является ли оно истинным или ложным, или, по крайней мере,
предполагать, что ему может быть приписана такая интерпретация. Примеры высказываний
приведены ниже.
   1. "Река Волга впадает в Каспийское море".
   2. "Все жители Земли имеют рост более двух метров".
   3. "В Африке находятся более десяти еще не известных захоронений фараонов Египта".
      Первое из приведенных высказываний является истинным, второе - ложным. Истинность
третьего высказывания не определена, но можно предполагать, что оно обязательно либо
истинно, либо ложно.
      Формальная аксиоматическая теория (в нашем случае - ИВ) считается заданной, если
выполнены условия, перечисленные ниже.
      1. Определено некоторое счетное множество символов. Таковыми в ИВ являются:
      а) x1 , x2 , ... , xn - пропозициональные переменные, представляющие элементарные
высказывания;
      б) & , v ,   , ¬ - логические символы;
      в) ( , ) - технические символы.
      Конечные последовательности символов называются выражениями.
      2. Определено подмножество выражений, называемых формулами. Дадим определение
формулы:
      а) xi -формула (i=1,n);
      б) если А и В - формулы, то А & В , A v B , А   В , Ā - формулы;
      в) других формул, кроме перечисленных в пп. а) и б), не существует.




                                               17