Nqthmเป็นโปรแกรมพิสูจน์ทฤษฎีบทบางครั้งเรียกว่าโปรแกรมพิสูจน์ทฤษฎีบท Boyer–Mooreมันเป็นโปรแกรมต้นแบบ^ของ ACL2 [ ^{1 ]}

ระบบนี้ได้รับการพัฒนาโดยโรเบิร์ต เอส. โบเยอร์และเจ. สโตรเธอร์ มัวร์ศาสตราจารย์ด้านวิทยาการคอมพิวเตอร์แห่งมหาวิทยาลัยเท็กซัส ออสตินพวกเขาเริ่มทำงานกับระบบนี้ในปี 1971 ที่เมืองเอดินบะระประเทศสกอตแลนด์เป้าหมายของพวกเขาคือการสร้างโปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติโดยใช้ตรรกะ พวกเขาใช้ภาษาPure LISP เวอร์ชันดัดแปลง เป็นตรรกะในการทำงาน

นิยามต่างๆ ถูกสร้างขึ้นในรูปแบบของฟังก์ชันเรียกซ้ำ โดยสมบูรณ์ ระบบนี้ใช้การเขียนใหม่และ วิธีการ อนุมาน อย่างกว้างขวาง ซึ่งจะใช้เมื่อการเขียนใหม่และสิ่งที่เรียกว่าการประเมินเชิงสัญลักษณ์ล้มเหลว

ระบบนี้สร้างขึ้นบนพื้นฐานของภาษา Lisp และมีความรู้พื้นฐานบางอย่างเกี่ยวกับสิ่งที่เรียกว่า "Ground-zero" ซึ่งเป็นสถานะของเครื่องหลังจากบูตระบบลงบนการใช้งาน Common Lisp

นี่เป็นตัวอย่างของการพิสูจน์ทฤษฎีบททางคณิตศาสตร์อย่างง่าย ฟังก์ชันTIMESเป็นส่วนหนึ่งของBOOT-STRAP (เรียกว่า "ดาวเทียม") และถูกกำหนดให้เป็น

( DEFN TIMES ( X Y ) ( IF ( ZEROP X ) 0 ( PLUS Y ( TIMES ( SUB1 X ) Y ))))

การกำหนดทฤษฎีบทนี้ยังแสดงด้วยไวยากรณ์ที่คล้ายกับภาษา Lisp ด้วย:

( พิสูจน์บทพิสูจน์การสลับที่ของเวลา( เขียนใหม่) ( เท่ากับ( เวลาx z ) ( เวลาz x )))

หากทฤษฎีบทนี้ได้รับการพิสูจน์ว่าเป็นจริง มันจะถูกเพิ่มเข้าไปในฐานความรู้ของระบบและสามารถใช้เป็นกฎการเขียนใหม่สำหรับการพิสูจน์ในอนาคตได้

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

การพิสูจน์สมบัติการสลับที่ของเวลายังคงดำเนินต่อไป:

ตั้งชื่อสมมติฐานนี้ว่า *1. เราจะใช้วิธีการอุปมาน โดยมีเงื่อนไขสองประการที่ได้จากข้อสันนิษฐานนี้ ซึ่งทั้งสองอย่างนั้นมีข้อบกพร่อง เราจึงจำกัดการพิจารณาของเราไว้เพียงสองข้อที่เสนอโดย จำนวนฟังก์ชันเรียกซ้ำที่ไม่ใช่แบบดั้งเดิมที่มากที่สุดในสมมติฐาน เนื่องจากทั้งสอง สิ่งเหล่านี้มีโอกาสเกิดขึ้นเท่ากัน เราจะเลือกโดยพลการ เราจะใช้วิธีอุปนัยตาม... แผนผังต่อไปนี้: (และ (หมายความว่า (ศูนย์ X) (p XZ)) (หมายความว่า (และ (ไม่ใช่ (ZEROP X)) (p (SUB1 X) Z)) (p XZ))) เลขคณิตเชิงเส้น บทพิสูจน์ COUNT-NUMBERP และนิยามของ ZEROP ให้ข้อมูลเกี่ยวกับ บอกเราว่าค่าที่วัดได้ (จำนวน X) ลดลงตามความสัมพันธ์ที่มีพื้นฐานที่ดี LESSP ในแต่ละขั้นตอนการเหนี่ยวนำของแผนการเหนี่ยวนำข้างต้น นำไปสู่ข้อสันนิษฐานใหม่สองข้อดังต่อไปนี้: กรณีที่ 2. (หมายความว่า (ZEROP X) (เท่ากับ (คูณ XZ) (คูณ ZX))) 

และหลังจากผ่านการพิสูจน์โดยการอุปมานหลายขั้นตอน ในที่สุดก็สรุปได้ว่า

กรณีที่ 1. (หมายความว่า (และ (ไม่ใช่ (ศูนย์ Z)) (เท่ากับ 0 (คูณ (SUB1 Z) 0))) (เท่ากับ 0 (คูณ Z 0))) วิธีนี้จะทำให้ความหมายของศูนย์ คูณ บวก และเท่ากับ ง่ายขึ้น โดยขยายความหมายออกไปดังนี้: ที. นั่นเป็นการเสร็จสิ้นการพิสูจน์ข้อ *1.1 ซึ่งเป็นการเสร็จสิ้นการพิสูจน์ข้อ *1 ด้วยเช่นกัน QED [ 0.0 1.2 0.5 ] ความเท่าเทียมกันของเวลา 

มีการตรวจสอบหรือยืนยันหลักฐานหลายอย่างกับระบบแล้ว โดยเฉพาะอย่างยิ่ง

• (1971) การเชื่อมต่อรายการ
• (1973) การเรียงลำดับแบบแทรก
• (1974) ตัวบวกเลขฐานสอง
• (1976) คอมไพเลอร์นิพจน์สำหรับเครื่องสแต็ก
• (1978) ความเป็นเอกลักษณ์ของการแยกตัวประกอบเฉพาะ
• (1983) ความสามารถในการผกผันของอัลกอริทึมการเข้ารหัส RSA
• (1984) ความไม่สามารถแก้ปัญหาการหยุดทำงานสำหรับ Pure Lisp
• (1985) ไมโครโปรเซสเซอร์ FM8501 (วอร์เรน ฮันท์) ^{[ 2 ]}
• (1986) ทฤษฎีบทความไม่สมบูรณ์ของเกอเดล (ชานการ์)
• (1988) CLI Stack (บิล เบเวียร์, วอร์เรน ฮันท์, แมตต์ คอฟแมนน์, เจ มัวร์, บิล ยัง)
• (1990) กฎการผกผันกำลังสองของเกาส์ (เดวิด รัสซินอฟฟ์)
• (1992) นายพลไบแซนไทน์และการซิงโครไนซ์นาฬิกา (เบเวียร์และยัง)
• (1992) คอมไพเลอร์สำหรับส่วนย่อยของภาษา Nqthm (อาร์เธอร์ แฟลทาว)
• (1993) โปรโตคอลการสื่อสารแบบอะซิงโครนัสแบบสองเฟส
• (1993) Motorola MC68020 และ Berkeley C String Library (หยวนหยู)
• (1994) ทฤษฎีบทปารีส-แฮร์ริงตัน แรมซีย์ ( เคนเนธ คูเนน )
• (1996) ความเท่าเทียมกันของ NFSA และ DFSA ( Debora Weber-Wulff )

แมตต์ คอฟแมนน์ได้พัฒนาเวอร์ชันที่มีประสิทธิภาพมากขึ้น เรียกว่า PC-Nqthm (Proof-checker Nqthm) เวอร์ชันนี้มอบเครื่องมือพิสูจน์ที่ระบบใช้โดยอัตโนมัติให้กับผู้ใช้ เพื่อให้สามารถให้คำแนะนำเพิ่มเติมแก่การพิสูจน์ได้ ซึ่งเป็นประโยชน์อย่างมาก เนื่องจากระบบมีแนวโน้มที่จะวนเวียนอยู่กับการพิสูจน์แบบอุปนัยที่ไม่สิ้นสุด ซึ่งเป็นสิ่งที่ไม่ก่อให้เกิดประโยชน์

• Boyer, Robert S. ; Moore, J Strother (1998). คู่มือตรรกศาสตร์เชิงคำนวณ (ฉบับที่ 2). ซานดิเอโก : สำนักพิมพ์ Academic Press . ISBN 9780121229559. OCLC  38515159 .
• Boyer, RS ; Kaufmann, M. ; Moore, JS (มกราคม 1995). "โปรแกรมพิสูจน์ทฤษฎีบท Boyer-Moore และการปรับปรุงเชิงโต้ตอบ" . Computers & Mathematics with Applications . 29 (2): 27– 62 . สืบค้นเมื่อ29 พฤษภาคม 2025 .

ในปี พ.ศ. 2548 Robert S. Boyer , Matt KaufmannและJ Strother Mooreได้รับรางวัล ACM Software System Awardสำหรับผลงานของพวกเขาเกี่ยวกับตัวพิสูจน์ทฤษฎีบท Nqthm ^{[ 3 ]}

• ระบบการให้เหตุผลอัตโนมัติ NQTHM
• โปรแกรมพิสูจน์ทฤษฎีบทบอยเออร์-มัวร์ (NQTHM)
• แม้ว่าระบบจะไม่ได้รับการสนับสนุนอีกต่อไปแล้ว แต่ก็ยังสามารถใช้งานได้ที่[1]
• เวอร์ชันที่รันได้บนGitHub : [2]