Démonstration formelle
séquence finie de propositions dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Démonstration formelle?
Résumez cet article pour un enfant de 10 ans
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é.