Formeel bewijs

In de formele wetenschap is een formeel bewijs een eindige reeks proposities (goedgevormde formules in formele taal) binnen het kader van de beschrijving van formele systemen waarbij elke propositie door middel van afleidingsregels uit voorafgaande proposities of axiomas kan worden afgeleid. De uiteindelijke propositie is een stelling. Het afleiden van een stelling is een logisch gevolg van de voorafgaande formules. Een logische consequentie is het resultaat van het deductieve systeem van een formeel systeem.

Een automatische stellingbewijzer is een programma dat van een gegeven propositie een formeel bewijs probeert te vinden. Dit is echter een moeilijk probleem dat niet in het algemeen beslisbaar is. Bij interactieve bewijsvoering wordt het formele bewijs door de gebruiker geleverd en slechts gecontroleerd met behulp van de computer.