Démonstration formelle

Une démonstration formelle est une séquence finie de propositions (appelées formules bien formées dans le cas d'un langage formel) dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes dans la séquence par une règle d'inférence. La dernière proposition de la séquence est un théorème d'un système formel. La notion de théorème n'est en général pas effective, donc n'existe pas de méthode par laquelle nous pouvons à chaque fois trouver une démonstration d'une proposition donnée ou de déterminer s'il y en a une. Le concept de déduction naturelle est une généralisation de la notion de démonstration[1].

Le théorème est une conséquence syntaxique de toutes les formules bien formées qui la précèdent dans la démonstration. Pour qu'une formule bien formée soit présente dans le cadre d'une démonstration, elle doit être le résultat de l'application d'une règle de l'appareil déductif.

Les démonstration formelles sont souvent construits à l'aide d'ordinateurs en tant qu'assistants de preuve. De manière significative, ces preuves peuvent être vérifiées automatiquement, également par ordinateur. La vérification des démonstrations formelles est généralement simple, alors que trouver des démonstrations (démonstration automatique de théorèmes) est généralement informatiquement intraitable et/ou seulement semi-décidable, selon le système formel utilisé.