Computer-assisted proof (original) (raw)
Maschinengestütztes Beweisen (oder missverständlicher: automatisches Beweisen; ein Teilgebiet der automatischen Deduktion) basiert auf der Verwendung von Computerprogrammen zur Erzeugung und Überprüfung von mathematischen Beweisen logischer Theoreme. Im Unterschied zu einem Computerbeweis wird versucht, den gesamten formalen Beweis bestehend aus Schritten und Zwischenergebnissen zu konstruieren.
| Property | Value |
|---|---|
| dbo:abstract | Maschinengestütztes Beweisen (oder missverständlicher: automatisches Beweisen; ein Teilgebiet der automatischen Deduktion) basiert auf der Verwendung von Computerprogrammen zur Erzeugung und Überprüfung von mathematischen Beweisen logischer Theoreme. Im Unterschied zu einem Computerbeweis wird versucht, den gesamten formalen Beweis bestehend aus Schritten und Zwischenergebnissen zu konstruieren. (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 idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the four color theorem was the first major theorem to be verified using a computer program. 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 automated 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, interactive proof assistants allow mathematicians to develop human-readable proofs which are nonetheless formally verified for correctness. Since these proofs are generally human-surveyable (albeit with difficulty, as with the proof of the Robbins conjecture) they do not share the controversial implications of computer-aided proofs-by-exhaustion. (en) Una prueba asistida por ordenador es una demostración matemática que ha sido generada al menos parcialmente utilizando una computadora. La mayoría de las pruebas asistidas por ordenador hasta la fecha han sido desarrollos de pruebas por exhaustación de un elevado número de casos asociados a un teorema matemático. La idea es usar un programa de computadora para realizar cálculos largos y proporcionar una prueba de que el resultado de estos cálculos implica el teorema dado. En 1976, el teorema de los cuatro colores fue el primer teorema importante que se verificó con un programa informático. También se han realizado intentos en el área de investigación de la inteligencia artificial para crear pruebas más pequeñas, explícitas y nuevas de teoremas matemáticos de abajo hacia arriba usando técnicas de razonamiento automático, como la búsqueda . Tales demostraciones automáticas de teoremas han demostrado numerosos nuevos resultados y han encontrado nuevas pruebas para teoremas conocidos. Además, la demostración interactiva de teoremas permite a los matemáticos desarrollar pruebas legibles para los seres humanos que, no obstante, se verifican formalmente para verificar su exactitud. Dado que estas pruebas son generalmente revisables por los matemáticos (aunque no sin dificultades, como con la prueba de la ) no comparten las implicaciones controvertidas de las pruebas asistidas por ordenador mediante agotamiento. (es) 컴퓨터를 이용한 증명은 수학적 증명 과정에 컴퓨터를 이용한 계산이 포함되어 있는 경우를 의미한다. 대표적인 경우로 4색정리가 있다. 증명 과정에서 컴퓨터를 이용하는 경우는 보통 사람이 직접 계산하기에는 힘든 것을 컴퓨터로 대신 처리하는 경우로, 예를 들어 4색 정리의 경우 무한개의 지도를 약 1500개의 경우로 분류한 다음 각각의 경우를 컴퓨터로 모두 계산해, 1200시간을 들여 검증했다. 이러한 증명의 가장 큰 문제점은 컴퓨터가 처리한 계산에 오류가 없는지 검증하는 것이 거의 불가능하다는 것이다. 검증을 위한 프로그램과 그 프로그램을 실행하는 CPU에 버그가 들어있을 수도 있기 때문에 잘못된 결론이 나올 수 있다는 것이다. 또한 이러한 방식의 증명은 수학적 발전에 도움이 거의 되지 않기 때문에 좋은 증명이 아니라는 비판이 있다. 필립 데이비스는 4색 정리를 컴퓨터로 증명했다는 것에 대해 '결국 [그 문제는] 좋은 문제가 아니었다'고 언급했다. (ko) 計算機援用証明とは、コンピュータによって少なくとも一部が生成された数学的証明である。今日における計算機援用証明のほとんどは数学的定理に対するの実装である。具体的には、膨大で複雑な計算をコンピュータによって実行し、計算結果が与えられた定理の主張を裏付けることを示す試みである。1976年に示された四色定理が計算機援用証明によって示された最初の定理である。計算機援用証明は人工知能の分野でも使われ、簡明かつ陽的で新しい（数学の）定理の証明を作り出すことが目指された。このような自動定理証明機はいくつかの新しい結果を生み出し、既存の定理に対しても新しい証明を発見した。 (ja) Доказательные вычисления — целенаправленные вычисления на ЭВМ, комбинируемые с аналитическими исследованиями, которые приводят к строгому установлению новых фактов и доказательству теорем. (ru) Доказові обчислення — цілеспрямовані комп'ютерні обчислення, комбіновані з аналітичними дослідженнями, які призводять до строгого встановлення нових фактів і доведення теорем. (uk) 電腦協助證明是一種部份或全部內容以電腦協助之數學證明。 (zh) |
| dbo:wikiPageExternalLink | https://www.comp.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html http://www.post-gazette.com/businessnews/2007/01/12/Number-proofs-done-by-computer-might-err/stories/200701120255%7Carchive-url=https:/web.archive.org/web/20180416201308/http:/www.post-gazette.com/businessnews/2007/01/12/Number-proofs-done-by-computer-might-err/stories/200701120255 https://apps.dtic.mil/sti/pdfs/ADA155378.pdf https://web.archive.org/web/20120717094035/https:/www.comp.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html https://www.ams.org/journals/bull/1982-06-03/S0273-0979-1982-15008-X/S0273-0979-1982-15008-X.pdf https://www.ams.org/notices/200811/%7Cwork=Notices |
| dbo:wikiPageID | 2840305 (xsd:integer) |
| dbo:wikiPageLength | 17712 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1112898378 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Projective_plane dbr:Proof_assistant dbr:Quasi-empiricism_in_mathematics dbr:Scientific_method dbc:Automated_theorem_proving dbr:DPLL_algorithm dbr:University_of_Edinburgh dbr:Validated_numerics dbc:Artificial_intelligence dbr:Computer dbr:Connect_Four dbr:Mitchell_Feigenbaum dbr:Model_checking dbr:NP-hard dbr:Theorem dbr:Erdős_discrepancy_problem dbr:Optimal_solutions_for_Rubik's_Cube dbr:Logic_Theorist dbr:Smale's_problems dbr:Computer_program dbr:Theoretical_physics dbr:Observational_study dbr:Minimum-weight_triangulation dbr:American_Mathematical_Society dbc:Numerical_analysis dbc:Argument_technology dbr:FPGA dbr:Formal_verification dbr:Four_color_theorem dbr:Kazhdan's_property_(T) dbr:Proof_by_exhaustion dbr:Mathematical_proof dbr:Interval_arithmetic dbr:Terence_Tao dbr:Happy_Ending_problem dbr:Artificial_intelligence dbc:Formal_methods dbc:Philosophy_of_mathematics dbr:Keller's_conjecture dbr:Kepler_conjecture dbr:Symbolic_computation dbr:Heuristic_(computer_science) dbr:Automated_theorem_prover dbr:Double_bubble_conjecture dbr:Automated_reasoning dbr:Automorphism_group_of_a_free_group dbr:Marijn_Heule dbr:Boolean_Pythagorean_triples_problem dbc:Computer-assisted_proofs dbr:Warwick_Tucker dbr:Petabytes dbr:Terabytes dbr:Metamath dbr:Seventeen_or_Bust dbr:Thomas_Tymoczko dbr:Verification_and_validation dbr:Experimental_mathematics dbr:Distributed_SAT-solver dbr:Exercise_(mathematics) dbr:Gigabyte dbr:Kolmogorov-Arnold-Moser_theorem dbr:Non-surveyable_proof dbr:SAT-solver dbr:Sudoku dbr:Schur's_theorem dbr:Van_der_Waerden_number dbr:Proof_checker dbr:Lorenz_attractor dbr:Mathematical_Platonism dbr:Mathematical_elegance dbr:Robbins_conjecture |
| dbp:wikiPageUsesTemplate | dbt:Cite_techreport dbt:Citation_needed dbt:Cite_book dbt:Cite_journal dbt:Cite_news dbt:Cite_thesis dbt:Cite_web dbt:Cn dbt:Columns-list dbt:Main dbt:More_citations_needed_section dbt:Reflist dbt:Short_description dbt:GBurl dbt:Clarify_span dbt:Mathematical_logic dbt:Numerical_PDE |
| dct:subject | dbc:Automated_theorem_proving dbc:Artificial_intelligence dbc:Numerical_analysis dbc:Argument_technology dbc:Formal_methods dbc:Philosophy_of_mathematics dbc:Computer-assisted_proofs |
| gold:hypernym | dbr:Proof |
| rdf:type | yago:WikicatMathematicalProofs yago:Ability105616246 yago:Abstraction100002137 yago:Argument106648724 yago:Cognition100023271 yago:Communication100033020 yago:Evidence106643408 yago:Indication106797169 yago:Know-how105616786 yago:MathematicalProof106647864 yago:Method105660268 yago:Proof106647614 yago:PsychologicalFeature100023100 dbo:TelevisionShow yago:WikicatFormalMethods |
| rdfs:comment | Maschinengestütztes Beweisen (oder missverständlicher: automatisches Beweisen; ein Teilgebiet der automatischen Deduktion) basiert auf der Verwendung von Computerprogrammen zur Erzeugung und Überprüfung von mathematischen Beweisen logischer Theoreme. Im Unterschied zu einem Computerbeweis wird versucht, den gesamten formalen Beweis bestehend aus Schritten und Zwischenergebnissen zu konstruieren. (de) 컴퓨터를 이용한 증명은 수학적 증명 과정에 컴퓨터를 이용한 계산이 포함되어 있는 경우를 의미한다. 대표적인 경우로 4색정리가 있다. 증명 과정에서 컴퓨터를 이용하는 경우는 보통 사람이 직접 계산하기에는 힘든 것을 컴퓨터로 대신 처리하는 경우로, 예를 들어 4색 정리의 경우 무한개의 지도를 약 1500개의 경우로 분류한 다음 각각의 경우를 컴퓨터로 모두 계산해, 1200시간을 들여 검증했다. 이러한 증명의 가장 큰 문제점은 컴퓨터가 처리한 계산에 오류가 없는지 검증하는 것이 거의 불가능하다는 것이다. 검증을 위한 프로그램과 그 프로그램을 실행하는 CPU에 버그가 들어있을 수도 있기 때문에 잘못된 결론이 나올 수 있다는 것이다. 또한 이러한 방식의 증명은 수학적 발전에 도움이 거의 되지 않기 때문에 좋은 증명이 아니라는 비판이 있다. 필립 데이비스는 4색 정리를 컴퓨터로 증명했다는 것에 대해 '결국 [그 문제는] 좋은 문제가 아니었다'고 언급했다. (ko) 計算機援用証明とは、コンピュータによって少なくとも一部が生成された数学的証明である。今日における計算機援用証明のほとんどは数学的定理に対するの実装である。具体的には、膨大で複雑な計算をコンピュータによって実行し、計算結果が与えられた定理の主張を裏付けることを示す試みである。1976年に示された四色定理が計算機援用証明によって示された最初の定理である。計算機援用証明は人工知能の分野でも使われ、簡明かつ陽的で新しい（数学の）定理の証明を作り出すことが目指された。このような自動定理証明機はいくつかの新しい結果を生み出し、既存の定理に対しても新しい証明を発見した。 (ja) Доказательные вычисления — целенаправленные вычисления на ЭВМ, комбинируемые с аналитическими исследованиями, которые приводят к строгому установлению новых фактов и доказательству теорем. (ru) Доказові обчислення — цілеспрямовані комп'ютерні обчислення, комбіновані з аналітичними дослідженнями, які призводять до строгого встановлення нових фактів і доведення теорем. (uk) 電腦協助證明是一種部份或全部內容以電腦協助之數學證明。 (zh) 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 idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the four color theorem was the first major theorem to be verified using a computer program. (en) Una prueba asistida por ordenador es una demostración matemática que ha sido generada al menos parcialmente utilizando una computadora. La mayoría de las pruebas asistidas por ordenador hasta la fecha han sido desarrollos de pruebas por exhaustación de un elevado número de casos asociados a un teorema matemático. La idea es usar un programa de computadora para realizar cálculos largos y proporcionar una prueba de que el resultado de estos cálculos implica el teorema dado. En 1976, el teorema de los cuatro colores fue el primer teorema importante que se verificó con un programa informático. (es) |
| rdfs:label | Maschinengestütztes Beweisen (de) Prueba asistida por ordenador (es) Computer-assisted proof (en) Preuve assistée par ordinateur (fr) 計算機援用証明 (ja) 컴퓨터를 이용한 증명 (ko) Доказательные вычисления (ru) 電腦協助證明 (zh) Доказові обчислення (uk) |
| owl:sameAs | freebase:Computer-assisted proof dbpedia-de:Computer-assisted proof yago-res:Computer-assisted proof wikidata:Computer-assisted proof dbpedia-es:Computer-assisted proof dbpedia-fr:Computer-assisted proof dbpedia-ja:Computer-assisted proof dbpedia-ko:Computer-assisted proof dbpedia-mk:Computer-assisted proof dbpedia-ru:Computer-assisted proof dbpedia-uk:Computer-assisted proof dbpedia-zh:Computer-assisted proof https://global.dbpedia.org/id/DCG6 |
| prov:wasDerivedFrom | wikipedia-en:Computer-assisted_proof?oldid=1112898378&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Computer-assisted_proof |
| is dbo:genre of | dbr:INTLAB |
| is dbo:wikiPageRedirects of | dbr:List_of_computer-assisted_proofs dbr:Computer-aided_proof dbr:Computer_assisted_proof dbr:Computer_proof |
| is dbo:wikiPageWikiLink of | dbr:Proof_assistant dbr:Argument_from_reason dbr:List_of_computer-assisted_proofs dbr:Validated_numerics dbr:Index_of_robotics_articles dbr:List_of_long_mathematical_proofs dbr:List_of_mathematics_awards dbr:Timeline_of_computational_mathematics dbr:Computer_algebra dbr:Mathematics dbr:Oren_Patashnik dbr:Conjecture dbr:Optimal_solutions_for_Rubik's_Cube dbr:1976_in_science dbr:Combinatorial_game_theory dbr:Computer-aided dbr:Timeline_of_scientific_computing dbr:Werner_Boy dbr:Minimum-weight_triangulation dbr:3D_tic-tac-toe dbr:Figure-eight_knot_(mathematics) dbr:Chua's_circuit dbr:Four_color_theorem dbr:Kazhdan's_property_(T) dbr:Natural_deduction dbr:Proof_by_exhaustion dbr:Hilbert's_problems dbr:Hyperbolic_Dehn_surgery dbr:Philosophy_of_computer_science dbr:Keller's_conjecture dbr:Automated_Mathematician dbr:Boolean_Pythagorean_triples_problem dbr:Raph_Levien dbr:Seventeen_or_Bust dbr:Series_(mathematics) dbr:Tensor_rank_decomposition dbr:Euler's_Gem dbr:Experimental_mathematics dbr:INTLAB dbr:Oscar_Lanford dbr:Finite_geometry dbr:Non-surveyable_proof dbr:Ramon_E._Moore dbr:Outline_of_artificial_intelligence dbr:Computer-aided_proof dbr:Computer_assisted_proof dbr:Computer_proof |
| is dbp:genre of | dbr:INTLAB |
| is foaf:primaryTopic of | wikipedia-en:Computer-assisted_proof |