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