В логике , и , в частности , теориях доказательств , процедура доказательства для данной логики является систематическим способом получения доказательств в некоторых доказательствах исчисления в (доказательной) отчетности.
Типы используемых исчислений доказательств
Есть несколько типов исчислений доказательств. Наиболее популярными являются естественная дедукция , секвенциальные исчисления (т. Е. Системы типа Генцена ), системы Гильберта и семантические таблицы или деревья. Данная процедура доказательства нацелена на конкретное исчисление доказательств, но часто может быть переформулирована так, чтобы производить доказательства в других стилях доказательства.
Полнота
Процедура доказательства для логики считается завершенной, если она дает доказательство для каждого доказуемого утверждения. Теоремы логических систем обычно рекурсивно перечислимы , что подразумевает существование полной, но крайне неэффективной процедуры доказательства; однако процедура доказательства представляет интерес только в том случае, если она достаточно эффективна.
Столкнувшись с недоказуемым утверждением, полная процедура доказательства может иногда преуспевать в обнаружении и сигнализировании о его недоказуемости. В общем случае, когда доказуемость является полуразрешимым свойством, это невозможно, и вместо этого процедура будет расходиться (не завершаться).
Смотрите также
Рекомендации
- В. Куайн 1982 (1950). Методы логики . Harvard Univ. Нажмите.