@prefix rdf: . @prefix dbpedia: . @prefix ns2: . dbpedia:Computer-assisted_proof rdf:type ns2:FormalMethods . @prefix owl: . dbpedia:Computer-assisted_proof owl:sameAs . @prefix foaf: . @prefix ns5: . dbpedia:Computer-assisted_proof foaf:page ns5:Computer-assisted_proof . @prefix dbpprop: . dbpedia:Computer-assisted_proof dbpprop:reference , , . @prefix rdfs: . dbpedia:Computer-assisted_proof rdfs:label "Computerbeweis"@de , "Computer-assisted proof"@en , "Assistant de preuve"@fr ; dbpprop:abstract "En informatique (ou en math\u00E9matiques assist\u00E9es par informatique), un assistant de preuve est un logiciel permettant l'\u00E9criture et la v\u00E9rification de preuves math\u00E9matiques, soit sur des th\u00E9or\u00E8mes au sens usuel des math\u00E9matiques, soit sur des assertions relatives \u00E0 l'ex\u00E9cution de programmes informatiques. L'\u00E9criture de preuves enti\u00E8rement formelles est une activit\u00E9 extr\u00EAmement fastidieuse; de nombreuses \u00E9tapes qui seraient saut\u00E9es, car consid\u00E9r\u00E9es comme \u00E9videntes pour le lecteur familier des math\u00E9matiques, doivent \u00EAtre d\u00E9cortiqu\u00E9es dans les plus grands d\u00E9tails. 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\u00E8dent des proc\u00E9dures de d\u00E9cision dans des domaines souvent utilis\u00E9s et d\u00E9cidables; souvent, on leur ajoute des proc\u00E9dures de semi-d\u00E9cision (qui ne se terminent pas forc\u00E9ment avec succ\u00E8s). Une objection \u00E0 l'usage d'assistants de preuve est que, de toute fa\u00E7on, la s\u00E9curit\u00E9 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\u00E7onner qu'ils soient eux-m\u00EAmes bogu\u00E9s. Un assistant de preuve bogu\u00E9 peut permettre de d\u00E9montrer l'absurde. Certains assistants de preuve, comme Coq, produisent un terme de preuve dont la v\u00E9rification peut \u00EAtre d\u00E9l\u00E9gu\u00E9e \u00E0 un logiciel beaucoup plus simple qu'un assistant complet; ainsi, Coq produit des termes du Calcul des Constructions (inductives, \u00E0 pr\u00E9sent), un lambda-calcul typ\u00E9 d'ordre sup\u00E9rieur, dont on peut relativement facilement v\u00E9rifier s'ils sont correctement typ\u00E9s. Coq, de plus, a lui-m\u00EAme \u00E9t\u00E9 prouv\u00E9 dans Coq par son v\u00E9rificateur de d\u00E9monstrations, ce qui rend la confiance que l'on peut avoir dans ce logiciel un peu plus l\u00E9gitime. Note sur la terminologie: L'utilisation de preuve \u00E0 la place de d\u00E9monstration est, en toute rigueur, un anglicisme, en tant que traduction directe du mot \u00ABproof\u00BB, mais l'utilisation du mot \u00ABpreuve\u00BB fait maintenant partie du langage des sp\u00E9cialistes et cet article se plie \u00E0 cet usage. La difficult\u00E9 est d'autant plus grande que le mot \u00ABdemonstration\u00BB a un usage courant diff\u00E9rent en anglais."@fr , "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."@en , "Als Computerbeweis bezeichnet man den Beweis einer Behauptung, das hei\u00DFt einer mathematischen oder logischen Aussage, mit Hilfe eines Computerprogramms. Man verwendet den Begriff insbesondere f\u00FCr solche Beweise, die folgendes Schema aufweisen: Zun\u00E4chst 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\u00E4hlen endlich vieler (meist sehr vieler) F\u00E4lle entschieden werden kann. Die Reduktion von P auf E ist \u00FCblicherweise ein ganz normaler, informeller mathematischer Beweis. Erst im n\u00E4chsten Schritt kommt der Computer ins Spiel: Man schreibt ein Programm, das alle F\u00E4lle aufz\u00E4hlt (generate) und dann jeweils \u00FCberpr\u00FCft, ob f\u00FCr sie E tats\u00E4chlich 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\u00E4nden gibt es dabei auch ganz handfeste methodische. Ein psychologischer Einwand ist das Ideal einer kurzen, logischen Begr\u00FCndung, die von jedermann leicht nachvollzogen werden kann. Solche Beweise werden allerdings in der mathematischen Praxis immer seltener. Die Monsterbeweise der aktuellen mathematischen Forschung k\u00F6nnen in allen Teilen (einschlie\u00DFlich der benutzten Hilfss\u00E4tze) von keinem einzelnen Menschen mehr nachvollzogen werden. Eher hypothetisch ist der Einwand, dass der Compiler oder die Hardware einen Fehler haben k\u00F6nnte. 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\u00E4lle aufz\u00E4hlt, und die test-Phase tats\u00E4chlich die Eigenschaft E f\u00FCr 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\u00E4ter erheblich verbessert werden musste), war auch das Programm sehr intransparent und nicht formal verifiziert. Ein j\u00FCngerer 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\u00F6nnen. Beweispr\u00FCfung ist ein universelles, nur logik-abh\u00E4ngiges Problem, w\u00E4hrend generate-and-test-Algorithmen problemspezifisch sind. Es gibt daher gute Gr\u00FCnde, warum maschinengepr\u00FCften formalen Beweisen mehr zu trauen ist als Computerbeweisen. F\u00FCr den Vier-Farben-Satz ist mittlerweile ein formaler Beweis durch Georges Gonthier vorgelegt worden, f\u00FCr den formalen Beweis der Keplerschen Vermutung im Rahmen des Fly-Speck-Projektes existieren zur Zeit nur wesentliche Teile."@de ; rdfs:comment "Als Computerbeweis bezeichnet man den Beweis einer Behauptung, das hei\u00DFt einer mathematischen oder logischen Aussage, mit Hilfe eines Computerprogramms. Man verwendet den Begriff insbesondere f\u00FCr solche Beweise, die folgendes Schema aufweisen: Zun\u00E4chst 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\u00E4hlen endlich vieler (meist sehr vieler) F\u00E4lle entschieden werden kann."@de , "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."@en , "En informatique (ou en math\u00E9matiques assist\u00E9es par informatique), un assistant de preuve est un logiciel permettant l'\u00E9criture et la v\u00E9rification de preuves math\u00E9matiques, soit sur des th\u00E9or\u00E8mes au sens usuel des math\u00E9matiques, soit sur des assertions relatives \u00E0 l'ex\u00E9cution de programmes informatiques."@fr . @prefix skos: . @prefix ns9: . dbpedia:Computer-assisted_proof skos:subject ns9:Artificial_intelligence , ns9:Philosophy_of_mathematics , ns9:Formal_methods , ns9:Automated_theorem_proving . @prefix ns10: . dbpedia:Computer-assisted_proof dbpprop:hasPhotoCollection ns10:Computer-assisted_proof . dbpedia:Computer-aided_proof dbpprop:redirect dbpedia:Computer-assisted_proof . @prefix yago: . yago:Computer-assisted_proof owl:sameAs dbpedia:Computer-assisted_proof .