ผลต่างระหว่างรุ่นของ "การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์"
เนื้อหาที่ลบ เนื้อหาที่เพิ่ม
New page: '''การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์''' เป็น[[บทพิสูจน์ทฤษฎีทางคณิตศา... |
ไม่มีความย่อการแก้ไข |
||
บรรทัด 2:
บทพิสูจน์ที่ใช้คอมพิวเตอร์ช่วยส่วนใหญ่ในปัจจุบัน มักใช้วิธี[[การพิสูจน์โดยการลองทุกความเป็นไปได้]]ของทฤษฎีที่พยายามพิสูจน์อยู่ [[ทฤษฎีบทสี่สี]]เป็นทฤษฎีใหญ่อันแรกที่ถูกพิสูจน์ด้วยคอมพิวเตอร์
แนวคิดของวิธีการนี้ คือการให้คอมพิวเตอร์รับหน้าที่ทำการคำนวณอันยืดยาว โดยใช้เทคนิคเลขคณิตเชิงช่วงในการควบคุม ไม่ให้มีความผิดพลาดมากเกินไป นั่นคือ เราสามารถมองการคำนวณที่ซับซ้อน เป็นลำดับของการคำนวณพื้นฐาน (เช่น +, -, *, /) ผลที่ได้จากการคำนวณพื้นฐานแต่ละขั้นนี้ เป็นผลโดยประมาณเนื่องจากคอมพิวเตอร์มีความแม่นยำจำกัด อย่างไรก็ตาม เราสามารถสร้างช่วงของคำตอบที่ถูกต้องได้จากผลโดยประมาณนี้ จากนั้นเราสามารถดำเนินการขั้นตอนต่อๆไป โดยการทำการคำนวณระหว่างช่วงของตัวเลขแต่ละตัวที่ได้มา
นอกจากนี้ ในสาขาวิจัยทางด้าน[[ปัญญาประดิษฐ์]] ยังได้มีความพยายาม ที่จะสร้างบทพิสูจน์ใหม่ที่กระชับและชัดเจนกว่าเดิม โดยการใช้เทคนิค[[การให้เหตุผลโดยเครื่องจักร]] เช่น การค้นหาแบบ[[ฮิวริสติก (วิทยาการคอมพิวเตอร์)|ฮิวริสติก]] ตัวพิสูจน์โดยอัตโนมัติดังกล่าวนี้ ได้ช่วยพิสูจน์ทฤษฏีใหม่ๆ อีกทั้งยังสร้างบทพิสูจน์ใหม่ๆ ให้กับทฤษฏีที่เคยได้รับพิสูจน์มาแล้วอีกด้วย
== เป้าหมายเชิงปรัชญา ==
== ดูเพิ่มเติม ==
* [[การพิสูจน์ทฤษฏีโดยอัตโนมัติ]]
* [[คณิตศาสตร์เชิงสัญลักษณ์]]
* [[การตรวจสอบแบบจำลอง]]
* [[การตรวจสอบบทพิสูจน์]]
* [[การให้เหตุผลโดยอัตโนมัติ]]
* [[การทวนสอบเชิงรูปนัย]] (formal method)
* [[คณิตศาสตร์เชิงทดลอง]]
* [[วิทยาศาสตร์เชิงการสังเกต]]
* [[ขยะเข้า, ขยะออก]]
== อ่านเพิ่มเติม ==
* Lenat, D.B., (1976), AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Ph.D. Thesis, STAN-CS-76-570, and Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.
== ลิงก์ภายนอก ==
* Edmund Furse; [http://www.comp.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html Why did AM run out of steam?]
* Keith Devlin; [http://www.maa.org/devlin/devlin_01_05.html Last doubts removed about the proof of the Four Color Theorem], ''MAA Online'', January 2005
[[Category:ปัญญาประดิษฐ์]]
[[Category:วิธีการเชิงรูปนัย]] (formal method)
[[Category:ปรัชญาทางคณิตศาสตร์]]
[[Category:การพิสูจน์]]
[[en:Computer-assisted proof]]
| |||