This chapter presents a short surve

This chapter presents a short survey about the work that has been done on the Automath, is going on, and planned for the future. It also explains the concept of types and the matter of propositions as types and the survey is used to ventilate opinions and views in mathematics which are not easily set down in more technical reports. The project Automath develops a system of writing entire mathematical theories that verification of the correctness can be carried out by formal operations on the text. The motivations for the project: checking; understanding; and processing are discussed. These motives favor the choice of a system of a very general nature of formalizing mathematics of classical logic and set theory. One of the most important things in the project is that it expects machines to check the correctness of what humans have written. The machine has to find out whether there is a sequence of applications of the language rules that motivates the correctness of a line of the book.

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

บทนี้นำเสนอเป็นข้อคิดเห็นเกี่ยวกับงานที่ทำการบน Automath การ เกิดขึ้น และการวางแผนสำหรับอนาคต ยังอธิบายแนวคิดของชนิด และเรื่องของข้อเสนอเป็นประเภทและแบบสำรวจจะใช้การระบายอากาศความคิดเห็นและมุมมองในคณิตศาสตร์ซึ่งจะไม่ได้ตั้งค่าลงในรายงานทางเทคนิคเพิ่มเติม Automath โครงการพัฒนาระบบการเขียนทฤษฎีทางคณิตศาสตร์ทั้งที่การตรวจสอบความถูกต้องสามารถทำได้ โดยการดำเนินการอย่างเป็นทางการบนข้อความ แรงจูงใจสำหรับโครงการ: การตรวจสอบ ความเข้าใจ และมีการกล่าวถึงการประมวลผล แรงจูงใจเหล่านี้ชอบทางเลือกของระบบมากทั่วไปของ formalizing คณิตศาสตร์ตรรกะคลาสสิกและทฤษฎี สิ่งสำคัญสุดในโครงการอย่างใดอย่างหนึ่งเป็นที่คาดว่าเครื่องจะตรวจสอบความถูกต้องของสิ่งที่มนุษย์ได้เขียน เครื่องมีเพื่อค้นหาว่ามีลำดับของโปรแกรมประยุกต์ของกฎภาษา ที่จูงถูกต้องของบรรทัดของสมุดบัญชี

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

ในบทนี้จะนำเสนอแบบสำรวจสั้น ๆ เกี่ยวกับการทำงานที่ได้รับการทำใน Automath จะเกิดขึ้นและการวางแผนสำหรับอนาคต นอกจากนี้ยังอธิบายแนวคิดของชนิดและเรื่องของข้อเสนอกับประเภทและการสำรวจจะใช้ในการระบายอากาศคิดเห็นและมุมมองในวิชาคณิตศาสตร์ที่ยังไม่ได้ตั้งค่าได้ง่ายลงในรายงานทางเทคนิคเพิ่มเติม โครงการ Automath พัฒนาระบบการเขียนทฤษฎีทางคณิตศาสตร์ทั้งที่การตรวจสอบความถูกต้องสามารถดำเนินการได้โดยการดำเนินงานอย่างเป็นทางการในข้อความ แรงจูงใจสำหรับโครงการ: การตรวจสอบ; ความเข้าใจ และการประมวลผลที่จะกล่าวถึง แรงจูงใจเหล่านี้เข้าข้างทางเลือกของระบบของธรรมชาติทั่วไปมากของคณิตศาสตร์อย่างเป็นทางการของตรรกะคลาสสิกและตั้งทฤษฎี หนึ่งในสิ่งที่สำคัญที่สุดในโครงการที่เป็นที่คาดว่าเครื่องเพื่อตรวจสอบความถูกต้องของสิ่งที่มนุษย์ได้เขียน เครื่องมีเพื่อหาว่ามีลำดับของการใช้งานของกฎภาษาที่กระตุ้นความถูกต้องของบรรทัดของหนังสือที่

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

บทนี้นำเสนอแบบสำรวจสั้น ๆเกี่ยวกับ งานที่ได้ทำใน automath กำลัง และวางแผนสำหรับอนาคต มันยังอธิบายถึงแนวคิดของชนิดและประเภทของข้อเสนอที่สำคัญและใช้ระบายอากาศการสำรวจความคิดเห็นและมุมมองทางคณิตศาสตร์ที่ไม่ตั้งได้อย่างง่ายดายลงในรายงานทางเทคนิคเพิ่มเติม โครงการพัฒนาระบบ automath เขียนทฤษฎีทางคณิตศาสตร์ทั้งหมดที่มีการตรวจสอบความถูกต้องสามารถดำเนินการได้โดยการดำเนินงานอย่างเป็นทางการในข้อความ แรงจูงใจสำหรับโครงการตรวจสอบ ความเข้าใจ และประมวลผลได้ แรงจูงใจเหล่านี้สนับสนุนทางเลือกของระบบธรรมชาติทั่วไปมากของ formalizing คณิตศาสตร์ตรรกศาสตร์และทฤษฎีคลาสสิกชุด หนึ่งในสิ่งที่สำคัญที่สุดในโครงการที่คาดว่าเครื่องเพื่อตรวจสอบความถูกต้องของสิ่งที่มนุษย์เขียนไว้ เครื่องจะพบว่ามีลำดับของโปรแกรมภาษาของกฎที่ให้ความถูกต้องของบรรทัดของหนังสือ