Formální důkaz Ve formální logice a matematice je formální důkaz konečná posloupnost vět (ve formálním jazyce označovaných jako dobře utvořené vzorce), z nichž každá je axiom, předpoklad nebo vyplývá z předchozích vět v posloupnosti podle pravidla odvozování. Liší se od argumentu v přirozeném jazyce tím, že je přesný, jednoznačný a mechanicky ověřitelný. Pokud je množina předpokladů prázdná, pak se poslední větě ve formálním důkazu říká věta formálního systému. Pojem věty není obecně efektivní, takže nemusí existovat žádná metoda, kterou bychom vždy mohli najít důkaz dané věty nebo určit, že žádný neexistuje. Pojmy důkazu ve stylu Fichovy logiky, sekvenčního počtu a přirozené dedukce jsou zobecnění pojmu důkazu. Věta je syntaktický důsledek všech dobře utvořených vzorců, které jí v důkazu předcházejí. Aby se dobře utvořený vzorec mohl kvalifikovat jako součást důkazu, musí být výsledkem aplikace pravidla dedukčního aparátu (nějakého formálního systému) na předchozí dobře utvořené vzorce v důkazové posloupnosti. Formální důkazy se často konstruují s pomocí počítačů v interaktivním dokazování vět (například pomocí kontroly důkazů a automatizovaného dokazovače vět). Tyto důkazy lze významně kontrolovat automaticky, také pomocí počítače. Kontrola formálních důkazů je obvykle jednoduchá, zatímco problém nalezení důkazů (automatizované dokazování vět) je obvykle výpočetně nesnadný a/nebo pouze semidecidovatelný, v závislosti na použitém formálním systému.
Facebook Twitter