Общие положения

Логическое программирование и аксиоматические системы.

Теория формальных систем и, в частности, математическая логика являются формализацией человеческого мышления и представления наших знаний. Если предположить, что можно аксиоматизировать наши знания и можно построить алгоритм, позволяющий реализовать процесс вывода ответов на запрос из знаний, то в результате можно получить формальный метод для получения неформальных результатов.

Логическое программирование возникло в эру ЭВМ как естественное желание автоматизировать процесс логического вывода, поэтому оно является ветвью теории формальных систем.

Логическое программирование (в широком смысле) представляет собой семейство таких методов решения задач, в которых используются приемы логического вывода для манипулирования знаниями, представленными в декларативной форме[1]. Как писал Джордж Робинсон в 1984 году, в основе идеи логического программирования лежит описание задачи совокупностью утверждений на некотором формальном логическом языке и получение решения с помощью вывода в некоторой формальной (аксиоматической) системе. Такой аксиоматической системой являются исчисление предикатов первого порядка, поэтому в узком смысле логическое программирование понимается как использование исчисления предикатов первого порядка в качестве основы для описания предметной области и осуществления резолюционного логического вывода.

Аксиоматической системой называется способ задания множества путем указания исходных элементов (аксиом исчисления) и правил вывода, каждое из которых описывает, как строить новые элементы из исходных элементов.

Под аксиоматическим методом [7] понимают способ построения научной теории, при которой за ее основу берется ряд основополагающих, не требующих доказательств положений этой теории, называемыми аксиомами или постулатами.

Аксиоматический метод зародился в работах древнегреческих геометров. Вплоть до начала XIX века единственным образцом применения этого метода была геометрия Евклида.

В начале XIX века Н.И.Лобачевский и Я.Больяй, независимо друг от друга, открыли новую неевклидову геометрию, заменив пятый постулат о параллельных прямых на его отрицание. Их открытие стало отправной точкой для развития аксиоматического метода, который лег в основу теории формальных систем.

С накоплением опыта построения формальных теорий и попытками аксиоматизации арифметики, предпринятыми Дж. Пеано, возникла теория доказательств. Теория доказательств – это раздел современной математической логики и предшественница логического программирования.

Исчислениями называют наиболее важные из аксиоматических логических систем – исчисление высказываний и исчисление предикатов.

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