| 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
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 17712 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| 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
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:genre
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is dbp:genre
of | |
| is foaf:primaryTopic
of | |
