WikiDer > Процедура доказательства

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

Типы используемых исчислений доказательств

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

Полнота

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

Столкнувшись с недоказуемым утверждением, процедура полного доказательства может иногда успешно обнаружить и сигнализировать о его недоказуемости. В общем случае, когда доказуемость полуразрешимый свойство, это невозможно, и вместо этого процедура будет отклоняться (не завершаться).

Смотрите также

• Автоматическое доказательство теорем
• Сложность доказательства
• Доказательные таблицы
• Дедуктивная система
• Доказательство (правда)

использованная литература

• В. Куайн 1982 (1950). Методы логики. Harvard Univ. Нажмите.