Důkazní postup - Proof procedure

v logika, a zejména teorie důkazů, a důkazní postup za dané logika je systematická metoda výroby důkazů u některých důkazní kalkul (prokazatelných) prohlášení.

Druhy použitých důkazních kamenů

Existuje několik typů důkazních kamenů. Nejoblíbenější jsou přirozený odpočet, následující kalkul (tj., Gentzen systémy typu), Hilbertovy systémy, a sémantické výjevy nebo stromy. Daný postup kontroly se zaměří na konkrétní počet důkazů, ale lze jej často přeformulovat tak, aby poskytoval důkazy v jiných stylech důkazů.

Úplnost

Důkazový postup pro logiku je kompletní pokud předloží důkaz pro každé prokazatelné prohlášení. Věty logických systémů jsou obvykle rekurzivně spočetné, což znamená existenci úplného, ​​ale mimořádně neúčinného důkazního postupu; důkazní postup je však zajímavý, pouze pokud je přiměřeně efektivní.

Tváří v tvář neprokazatelnému prohlášení může někdy kompletní důkazní postup uspět při detekci a signalizaci jeho neprokázatelnosti. Obecně platí, že pokud je prokazatelnost a semidecidable vlastnost, to není možné a místo toho se procedura rozejde (ne ukončí).

Viz také

• Automatizované dokazování věty
• Složitost důkazu
• Důkazní tablo
• Deduktivní systém
• Důkaz (pravda)

Reference

• W. Quine 1982 (1950). Metody logiky. Harvard Univ. Lis.