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é.
Contexte
Langage formel
Un langage formel est un ensemble de suites finies de symboles. Un tel langage peut être défini sans référence à des significations de l'une de ses expressions; il peut exister avant qu'une interprétation lui soit attribué – c'est-à -dire, une signification. Les démonstrations formelles sont exprimées dans un langage formel.
Grammaire formelle
Une grammaire formelle (aussi appelée règles de formation) est une description précise des formules bien formées d'un langage formel. Elle est l'ensemble des chaînes sur l'alphabet du langage formel qui constituent les formules bien formées. Cependant, il ne décrit pas leur sémantique (à savoir, ce qu'ils signifient).
Système formel
Un système formel (également appelé un calcul logique ou un système logique) se compose d'un langage formel conjointement avec un système déductif. Le système déductif peut être constitué d'un ensemble de règles de transformation (également appelées règles d'inférence) ou d'un ensemble d'axiomes, ou les deux. Un système formel est utilisé pour dériver une expression d'une ou plusieurs autres expressions.
Interprétations
Une interprétation d'un système formel est l'attribution de signification aux symboles, et des valeurs aux suites d'un système formel. L'étude des interprétations est appelée la sémantique formelle. Donner une interprétation est synonyme de construction d'une structure.
Références
- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Formal proof » (voir la liste des auteurs).
- The Cambridge Dictionary of Philosophy, deduction
Liens externes
- « A Special Issue on Formal Proof », Notices of the American Mathematical Society,
- 2πix.com: Logic Une partie d'une série d'articles portant sur les mathématiques et la logique.