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.
Achtergrond
Formele taal
Formele taal is een eindige rij van symbolen. Deze symbolen worden over het algemeen ontworpen voordat ze een specifieke interpretatie krijgen, ofwel voordat er een bepaalde referent aan wordt gekoppeld.
Formele grammatica
Een formele grammatica is een beschrijving van de regels van een formele taal. Dit is een vrij breed begrip dat bijvoorbeeld op de informatica maar ook op de wiskundige logica betrekking kan hebben. De term "formele grammatica" wordt daarnaast soms ook gebruikt voor de regels van gewone menselijke taal (zie ook theoretische taalkunde). In het laatste geval heeft om spraakverwarring te vermijden de term grammatica echter de voorkeur.
Formeel systeem
Een formeel systeem, ook wel logisch systeem of logische calculus, bestaat uit formele taal in combinatie met een deductief systeem. Het deductieve systeem kan bestaan uit een reeks afleidingsregels, een reeks axioma's of een combinatie hiervan (in het laatste geval is sprake van de axiomatische methode). De bewijstheorie speelt in dit verband eveneens een belangrijke rol, namelijk bij het afleiden van de ene stelling uit de andere. Zie ook wiskundig bewijs.
Interpretaties
De interpretatie van een formeel systeem houdt het toekennen van betekenis aan symbolen in, zowel met betrekking tot natuurlijke als formele talen. In het laatste geval wordt van formele semantiek gesproken, in het eerste geval kortweg van semantiek.