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

Искусственный интеллект - это область вычислительной математики, которая занимается такими задачами. Вторая половина 60-х годов в области искусственного интеллекта выделялась особым увеличением интереса к машинному доказательству теорем. Широкое распространение и интенсивность этого интереса вызываются не только растущим сознанием, что умение делать логические выводы есть неотъемлемая часть человеческого интеллекта, но, возможно, в большей степени являются следствием того статуса, который приобрела техника машинного доказательства теорем в конце 60-х годов. Основы машинного доказательства теорем были заложены Эрбраном в 1930 г. Его метод был неосуществим практически до изобретения электронных вычислительных машин. Только после основополагающей статьи Дж. А. Робинсона в 1965 г. и развития метода резолюций были сделаны важные шаги к созданию программ, реализующих доказательство теорем. После 1965 г. были предложены многочисленные усовершенствования метода резолюций.

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

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

F₁: Если жарко и сыро, то будет дождь.

F₂: Если сыро, то жарко.

F₃: Сейчас сыро.

Вопрос: Будет ли дождь?

Приведенные выше утверждения записаны по-русски. Для их представления мы используем символы Р, Q и R, которые представляют понятия «жарко», «сыро» и «будет дождь» соответственно. Данные символы называются атомарными формулами или атомами. Кроме того, нам необходимы некоторые логических связок. В данном случае мы будем использовать знак "&", чтобы представить связку «и», и знак «®», чтобы представить связку «если ..., то». Тогда три приведенные выше утверждения представляются так:

F1: Р&Q®R,

F2: Q®R

F3: Q.

Таким образом, мы перевели русские утверждения на язык логических формул. В приведенном примере мы, по существу, должны были доказать, что некоторая формула логически следует из других формул. Утверждение о том, что некоторая формула логически следует из совокупности других формул; мы будем называть теоремой. Рассуждение, устанавливающее, что некоторая теорема верна, т. е. что формула логически следует из других формул, называется доказательством этой теоремы. Проблема машинного доказательства теорем состоит в рассмотрении машинных методов для нахождения доказательств теорем.

Есть много задач, которые удобно преобразовать в задачи доказательства теорем. Мы перечислим некоторые из них.

1. В вопросно-ответных системах утверждения могут быть представлены логическими формулами. Тогда, чтобы ответить на вопрос, используя данные факты, мы доказываем, что формула, соответствующая ответу, выводима из формул, представляющих эти факты.

2. В задаче анализа программ мы можем описать выполнение программы формулой А, а условие, что программа закончит работу, другой формулой В. Тогда проверка того, что программа закончит работу, эквивалентна доказательству того, что формула В следует из формулы А.

3. В проблеме изоморфизма графов мы хотим знать, изоморфен ли граф подграфу другого графа. Эта проблема не только представляет математический интерес, эта проблема практическая. Например, структура органического соединения может быть описана графом. Следовательно, проверка того, является ли подструктура структуры некоторого органического соединения структурой другого органического соединения, есть проблема изоморфизма. Для ее решения мы можем описать графы формулами. Таким образом, задача может быть сформулирована как задача доказательства того, что формула, представляющая граф, следует из формулы представляющей другой граф.

4. В проблеме преобразования состояний имеется набор состояний и набор операторов над состояниями. Когда один из операторов применяется к состоянию, получается новое состояние. Исходя из начального состояния, попытаемся найти последовательность операторов, которая преобразует начальное состояние в некоторое желаемое. В этом случае мы можем описать состояния и правила перехода логическими формулами. Следовательно, преобразование начального состояния в желаемое может рассматриваться как проверка того, что формула, представляющая желаемое состояние, следует из формулы, представляющей как состояния, так и правила перехода.

Логика - наука, изучающая методы доказательств и опровержений, т.е. методы установления истинности или ложности одних высказываний на основе истинности или ложности других высказываний. Математическая логика - это современная форма логики. Основными объектами логики являются высказывания. Существует два основных подхода к установлению истинности высказываний: эмпирический (опытный) и логический. При эмпирическом подходе истинность высказывания устанавливается с помощью некоторых проверяющих действий (наблюдений, измерений, экспериментов, документов, свидетелей и т.п.). Логический способ¹ заключается в том, что истинность высказываний устанавливается на основе истинности других высказываний, т.е. без обращения к фактам, а чисто формально, с помощью рассуждений. Анализ различных логических связей и методы построения на их основе правильных логических рассуждений - это и есть предмет логики. Рассмотрим простой пример. У вас есть настольная лампа с выключателем, включенная в розетку. Вы нажимаете кнопку выключателя, но лампочка не загорается. Тогда вы начинаете разбираться, в чем дело.

1. Как вам кажется, для того чтобы лампочка горела, необходимо совместное соблюдение следующих условий, каждое из которых есть высказывание:

"выключатель включен" - A

"лампочка исправна" - B₁

"выключатель исправен" - B₂

"вилка исправна" - B₃

"пробки в квартире исправны" - B₄.

Если A, B₁, B₂, B₃, B₄ имеют место, то лампочка должна гореть, т.е. высказывание C="лампочка горит" также истинно. Сказанное можно записать в виде сложного высказывания D=A&B₁&B₂&B₃&B₄C. Истинность данного высказывания вы и принимаете за эмпирическую истину.

2. Высказывание C ложно, т.е. лампочка не горит (факт, установленный наблюдением).

3. Если вы предполагаете, что D истинно, а при этом C ложно, следовательно ложно высказывание A&B₁&B₂&B₃B₄ (логическое рассуждение).

4. Отсюда следует, что ложно хотя бы одно из пяти высказываний A, B₁, B₂, B₃, B₄, т.е. истинно A B₁ B₂ B₃ B₄.

5. Поскольку A истинно (вы сами нажимали выключатель), опытным путем проверяете истинность остальных 4-х высказываний, т.е. ищете неисправность. В данном случае возможны следующие ситуации.

6. Высказывания B₁, B₂, B₃, B₄ оказываются истинными, а лампочка по-прежнему не горит. Логический вывод - гипотеза D неверна и нуждается в пересмотре (например нужно учесть еще две неисправности, не вошедшие в D: в шнуре и патроне). Принимаем новую гипотезу и рассуждаем на ее основе.

7. Некоторые из высказываний B₁, B₂, B₃, B₄ оказываются ложными. Устраняете соответствующие неисправности и включаете выключатель. Если лампочка горит, то ремонт успешно закончен. Если же лампочка так и не загорелась, то как и в п.6, гипотеза неверна и ее нужно изменить.

Рассмотренные в примере рассуждения формально описываются в подразделе математической логики, называемой исчислением высказываний.

Исчисление высказываний² имеет дело с теми же логическими формулами, что и алгебра логики¹, но устроена совершенно по другому - как формальная система, с помощью которой из исходного множества формул, называемых аксиомами, выводятся с помощью правил вывода (или доказываются) другие формулы. Правила вывода - это правила вида "из формул (F₁,..., F_m) выводима формула G", или в форме символической записи (F₁,..., F₄)=>G. Формулы (F₁,..., F₄) называются посылками вывода, а G - заключением вывода. В каждом конкретном случае формулы F₁,..., F_m, G имеют конкретный вид. Существуют различные варианты исчисления высказываний, каждый из которых имеет свои аксиомы и свои правила вывода. Обычно используются два правила вывода¹⁵: правило подстановки и правило заключения, или Modus Ponens. Правило подстановки формулируется следующим образом: "из формулы F(A) выводима любая формула F(G), получающаяся заменой всех вхождений A в формуле F на произвольную формулу G". Правило Modus Ponens⁴ формально записывается в следующем виде (A, A B)=>B и раскрывается следующим образом: если известна импликация A B и получен факт A, то можно вывести факт B. Оба правила широко используются во всех логических (формальных и неформальных) рассуждениях. Правило подстановки позволяет формулировать логические законы как соотношения между простыми высказываниями, а затем распространять эти законы на любые сложные высказывания. На практике алгебра логики используется чаще, чем исчисление высказываний. Однако исчисление высказываний имеет очень важное значение для логики, т.к. лежит в основе всех более сложных логических исчислений. Одним из таких исчислений является логика предикатов. Здесь наряду с высказываниями рассматриваются высказывательные функции или предикаты. Приведем некоторые примеры.

1. Выражение "x - простое число" не является высказыванием, хотя грамматически имеет форму высказывания. Из этого выражения можно получить высказывание после замены переменной x на определенное число. Таким образом данное выражение можно рассматривать как функцию P(x), зависящую от переменной x. Область определения P(x) - множество чисел, а область значений - высказывания.

2. Выражение "x больше y" можно рассматривать как функцию Q(x,y), зависящую от переменных x и y. Эта функция становится высказыванием после замены x и y на их значения.

Под предикатом от n переменных понимается выражение P(x₁,...,x_n), которое становится высказыванием при подстановке вместо переменных их значений из множеств M₁,..., M_n соответственно. Элементы множеств M₁,..., M_n называются предметами, а переменные x₁,..., x_n - предметными переменными. Однако из предикатов можно получать конкретные высказывания, не содержащие предметных констант, а утверждающие нечто обо всей предметной области. В естественном языке это делается с помощью оборотов "для всех x справедливо, что..." и "существует такой x, что ...". В языке формул логики предикатов этим оборотам соответствуют кванторы: квантор общности x и квантор существования x. Присоединение квантора с переменной x к предикатной формуле, содержащей x называется навешиванием квантора на переменную x. Переменная x при этом называется связанной; вместо нее подставлять константы уже нельзя. Например формула x P(x) означает "все числа простые". Это конкретное высказывание, которое ложно.

К предикатам можно применять операции алгебры высказываний² и получать новые предикаты.

Средства логики предикатов позволяют более обстоятельно проанализировать приведенную выше ситуацию с неисправной настольной лампой. Высказывания B₁, B₂, B₃, B₄ - это высказывания об исправности различных элементов электрической цепи. Если обозначить Q(x) предикат "x исправен", то эти высказывания запишутся как Q(лампочка), Q(выключатель), Q(вилка), Q(пробка), а гипотеза D - как формула A & xQ(x) C. Тогда тот факт, что B₁, B₂, B₃, B₄ истинны, а лампочка не горит, означает не ложность D, а всего лишь то, что истинность Q(x) проверена не для всех объектов предметной области. Гипотеза A& xQ(x) C остается при этом истинной, что говорит о ее большей общности по сравнению с D.

Как и в логике высказываний², в логике предикатов имеются эквивалентные соотношения, позволяющие преобразовывать предикатные формулы. Например, один квантор можно выразить через другой: ( xP(x))= x P(x), ( xP(x))= x P(x), а формулу, не содержащую переменной x, можно вынести за пределы действия квантора, связывающего x:; x(A F(x))=A xF(x); x(A&F(x))=A& xF(x).

В качестве аксиом обычно принимаются две формулы: xF(x) F(y)³, F(y) xF(x), где F(x) - любая предикатная формула, содержащая свободную переменную x, а в качестве правил вывода - правила, вводящие кванторы: F G(x) F xG(x), G(x) F xG(x) F. В этих правилах требуется, чтобы формула G(x) содержала свободную переменную x, а F ее не содержала.

Основы логики как науки были заложены древнегреческим ученым Аристотелем (4-й век до н.э.). Правила вывода (силлогизмы), описанные им, были основным инструментом логики вплоть до второй половины 19-го века. Рассмотрим известнейший аристотелевский силлогизм [12]:

Все люди смертны.

Сократ - человек.

____________________________

Следовательно, Сократ смертен.

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

x(P(x) Q(x)) - (1)

P(y) - (2)

Q(y) - (3)

Формальный вывод заключения (3) из посылок (1) и (2) состоит в следующем:

1. В первую предикатную аксиому³ вместо F(x) подставим P(x) Q(x). Получим

xP(x) Q(x)) (P(y) Q(y)). - (4)

2. Из формул (4) и (1) по правилу Modus Ponens⁴ следует, что выводима формула

P(y) Q(y). - (5)

3. Из формул (5) и (2) по правилу Modus Ponens выводима формула Q(y), что и требовалось доказать.

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