While theorem provers have become s

While theorem provers have become surprisingly powerful over the last decade, they are still too cumbersome to use and too limited in their capabilities to have any impact as teaching tools. As a case in point, see the recent study by Freek Wiedijk [12] where the fifteen major systems available today are challenged to prove that the square-root of 2 is irrational. One way around this problem is to use a hybrid system that combines a pure theorem prover with a computer algebra system, like Mathematica and Maple. In such hybrid systems the theorem prover organizes and controls the logical part of the argument whereas the computer algebra system takes care of all algebraic manipulations. Application of this rule shortens some proofs tremendously, and also brings the argument much closer to the form that a human prover would employ.

ผลลัพธ์ (ไทย) 1:

ในขณะที่เป็นทฤษฎีบท provers จู่ ๆ มีประสิทธิภาพมากกว่าทศวรรษ พวกเขาจะยังคงจำกัดในความสามารถของตนมีผลกระทบใด ๆ เป็นเครื่องมือในการสอนมากเกินไป และยุ่งยากเกินไปที่จะใช้ เป็นกรณีในจุด ดูการศึกษาล่าสุด โดย Freek Wiedijk [12] ซึ่งระบบหลักห้าว่างวันนี้จะท้าทายเพื่อพิสูจน์ว่า ที่รากที่ 2 เป็นจำนวนอตรรกยะ วิธีหนึ่งที่ปัญหานี้จะใช้ระบบไฮบริดที่ prover บริสุทธิ์ทฤษฎีบทเด่นพีชคณิตระบบคอมพิวเตอร์ Mathematica และเมเปิ้ล ในระบบไฮบริด prover ทฤษฎีบทจัด และควบคุมส่วนตรรกะของอาร์กิวเมนต์ในขณะที่ระบบพีชคณิตคอมพิวเตอร์ดูแล manipulations ภาพพีชคณิตทั้งหมด ประยุกต์ใช้กฎนี้ช่วยประหยัดหลักฐานบางอย่าง และยัง นำอาร์กิวเมนต์มากใกล้กับแบบฟอร์มที่จะจ้าง prover มนุษย์

ผลลัพธ์ (ไทย) 2:

ในขณะที่ provers ทฤษฎีบทได้กลายเป็นที่น่าแปลกใจที่มีประสิทธิภาพกว่าทศวรรษที่ผ่านมาพวกเขายังคงยุ่งยากเกินไปที่จะใช้และ จำกัด เกินไปในความสามารถของพวกเขาจะมีผลกระทบใด ๆ ที่เป็นเครื่องมือในการเรียนการสอน ในฐานะที่เป็นกรณีในจุดให้ดูที่การศึกษาล่าสุดโดย Freek Wiedijk [12] ที่สิบห้าระบบที่สำคัญมีอยู่ในปัจจุบันมีความท้าทายที่จะพิสูจน์ว่ารากที่ 2 ไม่ลงตัว วิธีการหนึ่งที่แก้ปัญหานี้คือการใช้ระบบไฮบริที่รวมทฤษฎีบทบริสุทธิ์ Prover กับระบบพีชคณิตคอมพิวเตอร์เช่น Mathematica และเมเปิ้ล ในระบบไฮบริดเช่น Prover ทฤษฎีบทจัดและควบคุมส่วนตรรกะของการโต้แย้งในขณะที่ระบบพีชคณิตคอมพิวเตอร์ดูแลกิจวัตรพีชคณิตทั้งหมด การประยุกต์ใช้กฎนี้ลดระยะพิสูจน์บางอย่างมากและยังนำข้อโต้แย้งมากใกล้ชิดกับรูปแบบที่ Prover มนุษย์จะจ้าง

ผลลัพธ์ (ไทย) 3:

ในขณะที่ทฤษฎีบท provers ได้กลายเป็นที่มีประสิทธิภาพน่าแปลกกว่าทศวรรษที่ผ่านมา พวกเขายังยุ่งยากในการใช้ก็จำกัดในความสามารถของพวกเขาที่จะมีผลกระทบใด ๆที่เป็นเครื่องมือการสอน เป็นกรณีในจุด เห็นผลการศึกษาล่าสุดโดย freek wiedijk [ 12 ] ที่ 15 หลักระบบที่มีอยู่ในปัจจุบันจะถูกท้าทายให้พิสูจน์ว่า รากที่สองของ 2 ที่ไร้เหตุผลวิธีหนึ่งที่ปัญหานี้คือการใช้ระบบไฮบริดที่ผสมผสานกับระบบโพรเวอร์บริสุทธิ์ทฤษฎีบทพีชคณิตคอมพิวเตอร์เช่น Mathematica กับเมเปิ้ล เช่นระบบไฮบริดทฤษฎีบทโพรเวอร์จัดและการควบคุมส่วนตรรกะของการโต้แย้งในขณะที่ระบบพีชคณิตคอมพิวเตอร์ดูแล manipulations พีชคณิตทั้งหมด การประยุกต์กฎนี้ shortens บางหลักฐานเป็นอย่างมากและยังทำให้อาร์กิวเมนต์ที่ใกล้ชิดมากกับรูปที่โพรเวอร์มนุษย์จะใช้