| dbpprop:abstract
|
- A computer-assisted proof is a mathematical proof that has been at least partially generated by computer. Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The four color theorem was the first major theorem to be proved using a computer. The idea of computer-assisted proofs is to use the computer to perform lengthy computations, but to verify the correctness of the program separately. Attempts have also been made in the area of artificial intelligence research to create smaller, explicit, new proofs of mathematical theorems from the bottom up using machine reasoning techniques such as heuristic search. Such automated theorem provers have proved a number of new results and found new proofs for known theorems. Additionally, some interactive proof assistants allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness. These areas do not share the controversial implications of computer-aided proofs-by-exhaustion.
- Als Computerbeweis bezeichnet man den Beweis einer Behauptung, das heißt einer mathematischen oder logischen Aussage, mit Hilfe eines Computerprogramms. Man verwendet den Begriff insbesondere für solche Beweise, die folgendes Schema aufweisen: Zunächst wird gezeigt, dass das allgemeine Problem P gilt, wenn eine andere Eigenschaft E gilt, also P auf E reduziert werden kann. Entscheidend ist dabei, dass E durch Aufzählen endlich vieler (meist sehr vieler) Fälle entschieden werden kann. Die Reduktion von P auf E ist üblicherweise ein ganz normaler, informeller mathematischer Beweis. Erst im nächsten Schritt kommt der Computer ins Spiel: Man schreibt ein Programm, das alle Fälle aufzählt (generate) und dann jeweils überprüft, ob für sie E tatsächlich gilt (test). Im Grunde wird E also durch eine Brute-Force-Methode entschieden. Aus beiden Teilen folgt dann die Behauptung P. Computerbeweise sind z. T. unter Mathematikern umstritten. Neben eher psychologischen oder hypothetischen Einwänden gibt es dabei auch ganz handfeste methodische. Ein psychologischer Einwand ist das Ideal einer kurzen, logischen Begründung, die von jedermann leicht nachvollzogen werden kann. Solche Beweise werden allerdings in der mathematischen Praxis immer seltener. Die Monsterbeweise der aktuellen mathematischen Forschung können in allen Teilen (einschließlich der benutzten Hilfssätze) von keinem einzelnen Menschen mehr nachvollzogen werden. Eher hypothetisch ist der Einwand, dass der Compiler oder die Hardware einen Fehler haben könnte. Durch Wiederholungen auf verschiedenen Rechnern und in verschiedenen Implementierungen kann dieses Risiko beliebig minimiert werden. Methodisch problematisch ist die Frage, ob das Programm den unterliegenden Algorithmus korrekt implementiert, ob der Algorithmus in der generate-Phase alle Fälle aufzählt, und die test-Phase tatsächlich die Eigenschaft E für diesen Fall zusichert. Hier hat man also ein handfestes Programmverifikationsproblem. Der erste bedeutende Computerbeweis war der des Vier-Farben-Satzes. Neben der Tatsache, dass die Problemreduktion als sehr unklar galt (und später erheblich verbessert werden musste), war auch das Programm sehr intransparent und nicht formal verifiziert. Ein jüngerer bedeutender Computerbeweis ist die erste Fassung der Keplerschen Vermutung. Ein Computerbeweis ist zu unterscheiden von einem Beweis durch einen Theorembeweiser (auch Beweis-Assistent genannt). Hierbei wird ein mathematischer Beweis formalisiert, d.h. soweit in eine Folge von logischen Einzelschritten zerlegt, dass diese von einem Computerprogramm nachvollzogen werden können. Beweisprüfung ist ein universelles, nur logik-abhängiges Problem, während generate-and-test-Algorithmen problemspezifisch sind. Es gibt daher gute Gründe, warum maschinengeprüften formalen Beweisen mehr zu trauen ist als Computerbeweisen. Für den Vier-Farben-Satz ist mittlerweile ein formaler Beweis durch Georges Gonthier vorgelegt worden, für den formalen Beweis der Keplerschen Vermutung im Rahmen des Fly-Speck-Projektes existieren zur Zeit nur wesentliche Teile.
- En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l'écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. L'écriture de preuves entièrement formelles est une activité extrêmement fastidieuse; de nombreuses étapes qui seraient sautées, car considérées comme évidentes pour le lecteur familier des mathématiques, doivent être décortiquées dans les plus grands détails. Cependant, l'assistant de preuve peut fournir plus ou moins d'automatisation pour limiter le travail de l'utilisateur humain. Certains assistants de preuve, tels que PVS, possèdent des procédures de décision dans des domaines souvent utilisés et décidables; souvent, on leur ajoute des procédures de semi-décision (qui ne se terminent pas forcément avec succès). Une objection à l'usage d'assistants de preuve est que, de toute façon, la sécurité des preuves obtenues repose sur le bon fonctionnement de l'assistant. En effet, les assistants de preuves sont de gros logiciels complexes, dont on peut soupçonner qu'ils soient eux-mêmes bogués. Un assistant de preuve bogué peut permettre de démontrer l'absurde. Certains assistants de preuve, comme Coq, produisent un terme de preuve dont la vérification peut être déléguée à un logiciel beaucoup plus simple qu'un assistant complet; ainsi, Coq produit des termes du Calcul des Constructions (inductives, à présent), un lambda-calcul typé d'ordre supérieur, dont on peut relativement facilement vérifier s'ils sont correctement typés. Coq, de plus, a lui-même été prouvé dans Coq par son vérificateur de démonstrations, ce qui rend la confiance que l'on peut avoir dans ce logiciel un peu plus légitime. Note sur la terminologie: L'utilisation de preuve à la place de démonstration est, en toute rigueur, un anglicisme, en tant que traduction directe du mot «proof», mais l'utilisation du mot «preuve» fait maintenant partie du langage des spécialistes et cet article se plie à cet usage. La difficulté est d'autant plus grande que le mot «demonstration» a un usage courant différent en anglais.
|
| rdfs:comment
|
- A computer-assisted proof is a mathematical proof that has been at least partially generated by computer. Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The four color theorem was the first major theorem to be proved using a computer. The idea of computer-assisted proofs is to use the computer to perform lengthy computations, but to verify the correctness of the program separately.
- Als Computerbeweis bezeichnet man den Beweis einer Behauptung, das heißt einer mathematischen oder logischen Aussage, mit Hilfe eines Computerprogramms. Man verwendet den Begriff insbesondere für solche Beweise, die folgendes Schema aufweisen: Zunächst wird gezeigt, dass das allgemeine Problem P gilt, wenn eine andere Eigenschaft E gilt, also P auf E reduziert werden kann. Entscheidend ist dabei, dass E durch Aufzählen endlich vieler (meist sehr vieler) Fälle entschieden werden kann.
- En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l'écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques.
|
![[RDF Data]](/statics/sw-cube.png)
