Azərbaycanca
Беларускі
Dansk
Deutsch
Española
Français
Indonesia
Italiana
日本語
Қазақ
Lietuvos
Nederlands
Português
Русский
සිංහල
แบบไทย
Türkçe
Українська
中國人
United State
Afrikaans
การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์ เป็นที่มีบางส่วนถูกสร้างขึ้นโดยคอมพิวเตอร์ บทพิสูจน์ที่ใช้คอมพิวเตอร์ช่วยส่วนใหญ่ในปัจจุบัน มักใช้วิธีของทฤษฎีที่พยายามพิสูจน์อยู่ ทฤษฎีบทสี่สีเป็นทฤษฎีใหญ่อันแรกที่ถูกพิสูจน์ด้วยคอมพิวเตอร์
แนวคิดของวิธีการนี้ คือการให้คอมพิวเตอร์รับหน้าที่ทำการคำนวณอันยืดยาว โดยใช้เทคนิคเลขคณิตเชิงช่วงในการควบคุม ไม่ให้มีความผิดพลาดมากเกินไป นั่นคือ เราสามารถมองการคำนวณที่ซับซ้อน เป็นลำดับของการคำนวณพื้นฐาน (เช่น +, -, *, /) ผลที่ได้จากการคำนวณพื้นฐานแต่ละขั้นนี้ เป็นผลโดยประมาณเนื่องจากคอมพิวเตอร์มีความแม่นยำจำกัด อย่างไรก็ตาม เราสามารถสร้างช่วงของคำตอบที่ถูกต้องได้จากผลโดยประมาณนี้ จากนั้นเราสามารถดำเนินการขั้นตอนต่อๆไป โดยการทำการคำนวณระหว่างช่วงของตัวเลขแต่ละตัวที่ได้มา
นอกจากนี้ ในสาขาวิจัยทางด้านปัญญาประดิษฐ์ ยังได้มีความพยายาม ที่จะสร้างบทพิสูจน์ใหม่ที่กระชับและชัดเจนกว่าเดิม โดยการใช้เทคนิค เช่น การค้นหาแบบฮิวริสติก ตัวพิสูจน์โดยอัตโนมัติดังกล่าวนี้ ได้ช่วยพิสูจน์ทฤษฏีใหม่ๆ อีกทั้งยังสร้างบทพิสูจน์ใหม่ๆ ให้กับทฤษฏีที่เคยได้รับพิสูจน์มาแล้วอีกด้วย
เป้าหมายเชิงปรัชญา
การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์ เป็นประเด็นที่มีการโต้เถียงกันมากในวงการคณิตศาสตร์ นักคณิตศาสตร์บางคนมีความเชื่อว่า บทพิสูจน์ที่ใช้คอมพิวเตอร์ช่วยอันแสนยืดยาวนั้น ไม่ถือเป็นจริงๆ เนื่องจากบทพิสูจน์แบบนี้ เต็มไปด้วยขั้นตอนการให้เหตุผลทางคณิตศาสตร์ ที่ยาวเกินกว่าที่มนุษย์จะ และรู้สึกว่านักคณิตศาสตร์ถูกบังคับให้ไว้ใจ ในการเขียนโปรแกรมคอมพิวเตอร์
ในทางกลับกัน เราสามารถถามคำถามโต้กลับได้ว่า หากมนุษย์ไม่ไว้ใจคอมพิวเตอร์ให้ทำการคำนวณอันยืดยาวแล้ว เหตุใดเราจึงไว้ใจในการใช้เหตุผลอันยืดยาวไม่แพ้กัน ของนักคณิตศาสตร์บางคน?
อ้างอิง
- 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; Why did AM run out of steam? 2006-05-28 ที่ เวย์แบ็กแมชชีน
- Keith Devlin; Last doubts removed about the proof of the Four Color Theorem 2005-02-06 ที่ เวย์แบ็กแมชชีน, MAA Online, January 2005 (formal method)
wikipedia, แบบไทย, วิกิพีเดีย, วิกิ หนังสือ, หนังสือ, ห้องสมุด, บทความ, อ่าน, ดาวน์โหลด, ฟรี, ดาวน์โหลดฟรี, mp3, วิดีโอ, mp4, 3gp, jpg, jpeg, gif, png, รูปภาพ, เพลง, เพลง, หนัง, หนังสือ, เกม, เกม, มือถือ, โทรศัพท์, Android, iOS, Apple, โทรศัพท์โมบิล, Samsung, iPhone, Xiomi, Xiaomi, Redmi, Honor, Oppo, Nokia, Sonya, MI, PC, พีซี, web, เว็บ, คอมพิวเตอร์
karphisucnthvsdibthdwykhxmphiwetxr epnthimibangswnthuksrangkhunodykhxmphiwetxr bthphisucnthiichkhxmphiwetxrchwyswnihyinpccubn mkichwithikhxngthvsdithiphyayamphisucnxyu thvsdibthsisiepnthvsdiihyxnaerkthithukphisucndwykhxmphiwetxr aenwkhidkhxngwithikarni khuxkarihkhxmphiwetxrrbhnathithakarkhanwnxnyudyaw odyichethkhnikhelkhkhnitechingchwnginkarkhwbkhum imihmikhwamphidphladmakekinip nnkhux erasamarthmxngkarkhanwnthisbsxn epnladbkhxngkarkhanwnphunthan echn phlthiidcakkarkhanwnphunthanaetlakhnni epnphlodypramanenuxngcakkhxmphiwetxrmikhwamaemnyacakd xyangirktam erasamarthsrangchwngkhxngkhatxbthithuktxngidcakphlodypramanni caknnerasamarthdaeninkarkhntxntxip odykarthakarkhanwnrahwangchwngkhxngtwelkhaetlatwthiidma nxkcakni insakhawicythangdanpyyapradisth yngidmikhwamphyayam thicasrangbthphisucnihmthikrachbaelachdecnkwaedim odykarichethkhnikh echn karkhnhaaebbhiwristik twphisucnodyxtonmtidngklawni idchwyphisucnthvstiihm xikthngyngsrangbthphisucnihm ihkbthvstithiekhyidrbphisucnmaaelwxikdwyepahmayechingprchyakarphisucnthvsdibthdwykhxmphiwetxr epnpraednthimikarotethiyngknmakinwngkarkhnitsastr nkkhnitsastrbangkhnmikhwamechuxwa bthphisucnthiichkhxmphiwetxrchwyxnaesnyudyawnn imthuxepncring enuxngcakbthphisucnaebbni etmipdwykhntxnkarihehtuphlthangkhnitsastr thiyawekinkwathimnusyca aelarusukwankkhnitsastrthukbngkhbihiwic inkarekhiynopraekrmkhxmphiwetxr inthangklbkn erasamarththamkhathamotklbidwa hakmnusyimiwickhxmphiwetxrihthakarkhanwnxnyudyawaelw ehtuideracungiwicinkarichehtuphlxnyudyawimaephkn khxngnkkhnitsastrbangkhn xangxingLenat 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 aehlngkhxmulxunEdmund Furse Why did AM run out of steam 2006 05 28 thi ewyaebkaemchchin Keith Devlin Last doubts removed about the proof of the Four Color Theorem 2005 02 06 thi ewyaebkaemchchin MAA Online January 2005 formal method