Логика вывода из гипотез в теории первого порядка

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

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

1. Прямое рассуждение. Предполагаем, что предикат-гипотеза Г (х) — истина в некоторой интерпретации, доказываем истинность В (х) в этой же интерпретации:

2. Обратное рассуждение. Неверно, что предикат-гипотеза Г (дг) — истина в некоторой интерпретации и В (х) ложно в этой же интерпретации:

3. Метод от противного. В предположении, что следствие В (х) ложно, в рассуждении доказывается, что Г (дг) ложно. Что противоречит прямому предположению, что Г (дг) истинно. Следовательно, следствие В (х) истинно:

Тогда, проверяя алгебраическими методами, по существу должны доказать равенство формул (ПГ,) В (х) — 0, или в логике —|(ПГ,) v В (х) = 1, что соответствует тавтологии.

Инверсная формула вывода ->Ф (.г) = /', & Р₂ & … & F_m & —*В (х) должна быть противоречием в логике.

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

Для заданных гипотез F_x, F_b…, F_m строится цепочка формул с применением правил вывода, пока не будет получена заданная формула В (х).