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

แม้ว่ารากฐานของตรรกศาสตร์ เชิงรูปธรรม จะย้อนกลับไปถึงอริสโตเติลแต่ช่วงปลายศตวรรษที่ 19 และต้นศตวรรษที่ 20 ได้เห็นการพัฒนาของตรรกศาสตร์สมัยใหม่และคณิตศาสตร์เชิงรูปธรรมBegriffsschriftของFrege (1879) ได้นำเสนอทั้งแคลคูลัสเชิงประพจน์ ที่สมบูรณ์ และสิ่งที่เป็นพื้นฐานของตรรกศาสตร์เชิงภาคแสดงสมัยใหม่[ 1 ^{] Foundations of} Arithmeticของเขาซึ่งตีพิมพ์ในปี 1884 ^{[ 2 ]}ได้แสดง (บางส่วนของ) คณิตศาสตร์ในตรรกศาสตร์เชิงรูปธรรม แนวทางนี้ได้รับการสานต่อโดยRussellและWhiteheadในPrincipia Mathematica ที่ทรงอิทธิพลของพวกเขา ซึ่งตีพิมพ์ครั้งแรกในปี 1910–1913 ^{[ 3 ]}และมีฉบับแก้ไขครั้งที่สองในปี 1927 ^{[ 4 ]} Russell และ Whitehead คิดว่าพวกเขาสามารถอนุมานความจริงทางคณิตศาสตร์ทั้งหมดได้โดยใช้สัจพจน์และกฎการอนุมานของตรรกศาสตร์เชิงรูปธรรม ซึ่งในทางทฤษฎีแล้วเป็นการเปิดกระบวนการนี้ไปสู่ระบบอัตโนมัติ^{[ 5 ]}ในปี พ.ศ. 2463 Thoralf Skolemได้ทำให้ผลลัพธ์ก่อนหน้านี้ของLeopold Löwenheim ง่ายขึ้น ซึ่งนำไปสู่ทฤษฎีบท Löwenheim–Skolemและในปี พ.ศ. 2473 นำไปสู่แนวคิดของจักรวาล Herbrandและการตีความ Herbrandที่อนุญาตให้(ความ) พอใจของสูตรลำดับที่หนึ่ง (และด้วยเหตุนี้ความถูกต้องของทฤษฎีบท) ลดลงเหลือปัญหาความพึงพอใจเชิงประพจน์ (ซึ่งอาจมีจำนวนอนันต์) ^{[ 6 ]}

ในปี พ.ศ. 2462 Mojżesz Presburgerได้แสดงให้เห็นว่าทฤษฎีลำดับที่หนึ่งของจำนวนธรรมชาติที่มีการบวกและความเท่าเทียมกัน (ปัจจุบันเรียกว่าเลขคณิต Presburgerเพื่อเป็นเกียรติแก่เขา) สามารถตัดสินได้และได้เสนออัลกอริทึมที่สามารถระบุได้ว่าประโยค ที่กำหนด ในภาษา นั้น เป็นจริงหรือเท็จ^{[ 7 ] [ 8 ]}

อย่างไรก็ตาม ไม่นานหลังจากผลลัพธ์เชิงบวกนี้เคิร์ท เกอเดล ได้ตีพิมพ์On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931) ซึ่งแสดงให้เห็นว่าในระบบสัจพจน์ที่แข็งแกร่งเพียงพอ จะมีข้อความที่เป็นจริงที่ไม่สามารถพิสูจน์ได้ในระบบ^{[ 9 ]}หัวข้อนี้ได้รับการพัฒนาเพิ่มเติมในช่วงทศวรรษ 1930 โดยอลอนโซ เชิร์ชและอลัน ทัวริง ซึ่งในด้านหนึ่งได้ให้คำจำกัดความของ ความสามารถในการคำนวณที่เป็นอิสระแต่เทียบเท่ากันสองแบบและในอีกด้านหนึ่งได้ให้ตัวอย่างที่เป็นรูปธรรมของคำถามที่ไม่สามารถตัดสินได้^{[ 10 ]}

ในปี พ.ศ. 2497 มาร์ติน เดวิสได้เขียนโปรแกรมอัลกอริทึมของเพรสเบอร์เกอร์สำหรับคอมพิวเตอร์หลอดสุญญากาศJOHNNIAC ที่สถาบันเพื่อการศึกษาขั้นสูงในพรินซ์ตัน รัฐนิวเจอร์ซีย์ ตามที่เดวิสกล่าวไว้ว่า "ความสำเร็จอันยิ่งใหญ่ของมันคือการพิสูจน์ว่าผลรวมของจำนวนคู่สองจำนวนเป็นจำนวนคู่" [ ^{8 ] [ 11 ] ระบบ} Logic Theoristในปี พ.ศ. 2499 ซึ่งเป็นระบบการอนุมานสำหรับตรรกะเชิงประพจน์ของPrincipia Mathematicaที่พัฒนาโดยอัลเลน นิวเวลล์ เฮอร์เบิร์ต เอ. ไซมอนและเจซี ชอว์ มี ความทะเยอทะยาน มากกว่า ระบบ Logic Theorist ทำงานบน JOHNNIAC เช่นกัน โดยสร้างบทพิสูจน์จากชุดของสัจพจน์เชิงประพจน์ขนาดเล็กและกฎการอนุมานสามข้อ ได้แก่modus ponens การแทนที่ตัวแปร (เชิงประพจน์) และการแทนที่สูตรด้วยคำจำกัดความ ระบบนี้ใช้ คำแนะนำ แบบฮิวริสติกและสามารถพิสูจน์ทฤษฎีบท 38 ข้อแรกจาก 52 ข้อของPrincipia ได้^{[ 8 ]}

แนวทาง "ฮิวริสติก" ของนักทฤษฎีตรรกศาสตร์พยายามเลียนแบบนักคณิตศาสตร์ของมนุษย์ และไม่สามารถรับประกันได้ว่าจะสามารถหาหลักฐานพิสูจน์สำหรับทฤษฎีบทที่ถูกต้องทุกข้อได้แม้ในทางทฤษฎี ในทางตรงกันข้าม อัลกอริทึมอื่นๆ ที่เป็นระบบมากกว่า บรรลุความสมบูรณ์สำหรับตรรกศาสตร์ลำดับที่หนึ่งอย่างน้อยในทางทฤษฎี แนวทางเริ่มต้นอาศัยผลลัพธ์ของHerbrandและSkolemในการแปลงสูตรลำดับที่หนึ่งเป็นชุดสูตรประพจน์ ที่ใหญ่ขึ้นเรื่อยๆ โดยการแทนค่าตัวแปรด้วยเทอมจากจักรวาลของ Herbrandจากนั้นสามารถตรวจสอบความไม่สามารถเป็นจริงของสูตรประพจน์ได้โดยใช้วิธีการต่างๆ โปรแกรมของ Gilmore ใช้การแปลงเป็นรูปแบบปกติแบบแยกส่วนซึ่งเป็นรูปแบบที่ความสามารถในการเป็นจริงของสูตรนั้นชัดเจน^{[ 8 ] [ 12 ]}

ขึ้นอยู่กับตรรกะพื้นฐาน ปัญหาในการตัดสินความถูกต้องของสูตรจะแตกต่างกันไปตั้งแต่เรื่องเล็กน้อยไปจนถึงเป็นไปไม่ได้ สำหรับกรณีทั่วไปของตรรกะเชิงประพจน์ปัญหาสามารถตัดสินได้แต่เป็นปัญหาco-NP-completeดังนั้นจึงเชื่อกันว่ามีเพียงอัลกอริทึมเวลาเลขชี้กำลัง เท่านั้นที่มีอยู่สำหรับงานพิสูจน์ทั่วไป ^{[ 13 ]}สำหรับแคลคูลัสเชิงประพจน์ลำดับที่หนึ่ง ทฤษฎีบทความสมบูรณ์ของ Gödelระบุว่าทฤษฎีบท (ข้อความที่พิสูจน์ได้) เป็นสูตรที่ถูกต้อง ตามความหมายอย่างแท้จริง ดังนั้นสูตรที่ถูกต้องจึงสามารถแจงนับได้ด้วยการคำนวณ กล่าวคือ หากมีทรัพยากรไม่จำกัด สูตรที่ถูกต้องใดๆ ก็สามารถพิสูจน์ได้ในที่สุด อย่างไรก็ตาม สูตร ที่ไม่ถูกต้อง (สูตรที่ไม่เป็นไปตามทฤษฎีที่กำหนด) ไม่สามารถรับรู้ได้เสมอไป^{[ 14 ]}

ข้างต้นใช้ได้กับทฤษฎีลำดับที่หนึ่ง เช่นพีชคณิตของ Peanoอย่างไรก็ตาม สำหรับแบบจำลองเฉพาะที่อาจอธิบายได้ด้วยทฤษฎีลำดับที่หนึ่ง บางข้อความอาจเป็นจริงแต่ไม่สามารถตัดสินได้ในทฤษฎีที่ใช้อธิบายแบบจำลองนั้น ตัวอย่างเช่น จากทฤษฎีบทความไม่สมบูรณ์ของ Gödelเราทราบว่าทฤษฎีที่สอดคล้องกันใดๆ ที่มีสัจพจน์ที่เป็นจริงสำหรับจำนวนธรรมชาติไม่สามารถพิสูจน์ข้อความลำดับที่หนึ่งทั้งหมดที่เป็นจริงสำหรับจำนวนธรรมชาติได้ แม้ว่ารายการสัจพจน์จะสามารถแจงนับได้เป็นอนันต์ก็ตาม^{[ 15 ]}เป็นผลให้โปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติจะไม่สามารถยุติการทำงานได้ในขณะที่กำลังค้นหาการพิสูจน์เมื่อข้อความที่กำลังตรวจสอบไม่สามารถตัดสินได้ในทฤษฎีที่ใช้ แม้ว่าจะเป็นจริงในแบบจำลองที่สนใจก็ตาม แม้จะมีข้อจำกัดทางทฤษฎีนี้ ในทางปฏิบัติ โปรแกรมพิสูจน์ทฤษฎีบทสามารถแก้ปัญหาที่ยากได้มากมาย แม้ในแบบจำลองที่ไม่ได้อธิบายอย่างสมบูรณ์โดยทฤษฎีลำดับที่หนึ่งใดๆ (เช่นจำนวนเต็ม )

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

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

ผู้ช่วยพิสูจน์ต้องใช้ผู้ใช้ที่เป็นมนุษย์ในการให้คำแนะนำแก่ระบบ ขึ้นอยู่กับระดับของระบบอัตโนมัติ ผู้พิสูจน์สามารถลดทอนลงเหลือเพียงผู้ตรวจสอบการพิสูจน์ โดยผู้ใช้ให้การพิสูจน์ในรูปแบบที่เป็นทางการ หรือสามารถดำเนินการพิสูจน์ที่สำคัญได้โดยอัตโนมัติ ผู้พิสูจน์แบบโต้ตอบใช้สำหรับงานที่หลากหลาย แต่แม้แต่ระบบอัตโนมัติเต็มรูปแบบก็ยังพิสูจน์ทฤษฎีบทที่น่าสนใจและยากจำนวนหนึ่ง รวมถึงอย่างน้อยหนึ่งทฤษฎีบทที่นักคณิตศาสตร์ไม่สามารถพิสูจน์ได้มาเป็นเวลานาน นั่นคือ ทฤษฎีบทคาดการณ์ของร็อบบินส์^{[ 16 ] [ 17 ]}อย่างไรก็ตาม ความสำเร็จเหล่านี้เกิดขึ้นเป็นครั้งคราว และการทำงานกับปัญหาที่ยากมักต้องใช้ผู้ใช้ที่มีความเชี่ยวชาญ

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

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

การใช้งานเชิงพาณิชย์ของการพิสูจน์ทฤษฎีบทอัตโนมัติส่วนใหญ่จะมุ่งเน้นไปที่ การออกแบบ และการตรวจสอบวงจรรวม นับตั้งแต่ เกิดข้อบกพร่องของ Pentium FDIV หน่วยประมวลผลจุดลอยตัวที่ซับซ้อนของไมโครโปรเซสเซอร์สมัยใหม่ได้รับการออกแบบด้วยการตรวจสอบอย่างเข้มงวดเป็นพิเศษAMD , Intelและบริษัทอื่นๆ ใช้การพิสูจน์ทฤษฎีบทอัตโนมัติเพื่อตรวจสอบว่าการหารและการดำเนินการอื่นๆ ได้รับการใช้งานอย่างถูกต้องในโปรเซสเซอร์ของพวกเขา^{[ 18 ]}

การใช้งานอื่นๆ ของตัวพิสูจน์ทฤษฎีบท ได้แก่การสังเคราะห์โปรแกรมการสร้างโปรแกรมที่ตรงตามข้อกำหนดอย่างเป็นทางการ [ ^{19 ] ตัว}พิสูจน์ทฤษฎีบทอัตโนมัติได้รับการบูรณาการเข้ากับผู้ช่วยพิสูจน์รวมถึงIsabelle/ HOL ^{[ 20 ]}

การประยุกต์ใช้ตัวพิสูจน์ทฤษฎีบทยังพบได้ในการประมวลผลภาษาธรรมชาติและความหมายเชิงรูปธรรมซึ่งใช้ในการวิเคราะห์การแสดงแทนวาทกรรม^{[ 21 ] [ 22 ]}

ในช่วงปลายทศวรรษ 1960 หน่วยงานที่ให้ทุนสนับสนุนการวิจัยด้านการอนุมานอัตโนมัติเริ่มเน้นย้ำถึงความจำเป็นในการประยุกต์ใช้ในทางปฏิบัติ หนึ่งในสาขาที่ประสบความสำเร็จเป็นครั้งแรกคือการตรวจสอบโปรแกรมโดยที่ตัวพิสูจน์ทฤษฎีบทลำดับแรกถูกนำไปใช้กับปัญหาการตรวจสอบความถูกต้องของโปรแกรมคอมพิวเตอร์ในภาษาต่างๆ เช่นPascal , Adaเป็นต้น ระบบตรวจสอบโปรแกรมในยุคแรกๆ ที่โดดเด่นคือ Stanford Pascal Verifier ที่พัฒนาโดยDavid Luckhamที่มหาวิทยาลัยสแตนฟอร์ด [ ^{23 ] [ 24 ] [ 25 ] ระบบ}นี้มีพื้นฐานมาจาก Stanford Resolution Prover ซึ่งพัฒนาขึ้นที่สแตนฟอร์ดเช่นกัน โดยใช้ หลักการ แก้ของJohn Alan Robinsonนี่เป็นระบบอนุมานอัตโนมัติระบบแรกที่แสดงให้เห็นถึงความสามารถในการแก้ปัญหาทางคณิตศาสตร์ที่ประกาศในNotices of the American Mathematical Societyก่อนที่จะมีการเผยแพร่คำตอบอย่างเป็นทางการ

การพิสูจน์ทฤษฎีบท ลำดับแรกเป็นหนึ่งในสาขาย่อยที่พัฒนามากที่สุดของการพิสูจน์ทฤษฎีบทอัตโนมัติ ตรรกะมีความสามารถในการแสดงออกเพียงพอที่จะอนุญาตให้ระบุปัญหาใดๆ ก็ได้ ซึ่งมักจะเป็นไปในลักษณะที่เป็นธรรมชาติและเข้าใจง่าย ในทางกลับกัน มันยังคงสามารถตัดสินได้บางส่วน และมีการพัฒนาแคลคูลัสที่สมบูรณ์และมีเหตุผลจำนวนมาก ทำให้ระบบอัตโนมัติ ทำงานได้ อย่างเต็มที่^{[ 26 ]}ตรรกะที่มีความสามารถในการแสดงออกมากกว่า เช่นตรรกะลำดับสูงช่วยให้สามารถแสดงปัญหาได้หลากหลายกว่าตรรกะลำดับแรก แต่การพิสูจน์ทฤษฎีบทสำหรับตรรกะเหล่านี้ยังไม่ได้รับการพัฒนาเท่าที่ควร^{[ 27 ] [ 28 ]}

มีการทับซ้อนกันอย่างมากระหว่างโปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติลำดับที่หนึ่งและโปรแกรมแก้ปัญหา SMTโดยทั่วไป โปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติจะเน้นที่การสนับสนุนตรรกะลำดับที่หนึ่งแบบเต็มรูปแบบที่มีตัวบ่งปริมาณ ในขณะที่โปรแกรมแก้ปัญหา SMT จะเน้นที่การสนับสนุนทฤษฎีต่างๆ (สัญลักษณ์ภาคแสดงที่ตีความ) มากกว่า โปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติจะเก่งในปัญหาที่มีตัวบ่งปริมาณจำนวนมาก ในขณะที่โปรแกรมแก้ปัญหา SMT จะทำได้ดีในปัญหาขนาดใหญ่ที่ไม่มีตัวบ่งปริมาณ^{[ 29 ]} เส้นแบ่งนั้นค่อนข้างคลุมเครือจนโปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติบางตัวเข้าร่วมใน SMT-COMP ในขณะที่ โปรแกรมแก้ปัญหา SMT บางตัวเข้าร่วมในCASC ^{[ 30 ]}

คุณภาพของระบบที่นำไปใช้ได้รับประโยชน์จากการมีอยู่ของคลัง ตัวอย่าง มาตรฐาน ขนาดใหญ่ — คลังปัญหาThousands of Problems for Theorem Provers (TPTP) ^{[ 31 ]} —รวมถึงจากการแข่งขันระบบ CADE ATP (CASC) ซึ่งเป็นการแข่งขันระบบลำดับแรกประจำปีสำหรับปัญหาลำดับแรกที่สำคัญหลายประเภท

ระบบสำคัญบางระบบ (ซึ่งทั้งหมดเคยได้รับรางวัลชนะเลิศอย่างน้อยหนึ่งประเภทในการแข่งขัน CASC) มีรายชื่ออยู่ด้านล่างนี้

• Eเป็นโปรแกรมพิสูจน์ประสิทธิภาพสูงสำหรับตรรกะลำดับที่หนึ่งแบบสมบูรณ์ แต่สร้างขึ้นบนแคลคูลัสเชิงสมการล้วนๆซึ่งพัฒนาขึ้นครั้งแรกในกลุ่มการให้เหตุผลอัตโนมัติของมหาวิทยาลัยเทคนิคแห่งมิวนิกภายใต้การกำกับดูแลของWolfgang Bibelและปัจจุบันอยู่ที่มหาวิทยาลัยสหกรณ์แห่งรัฐบาเดิน-เวือร์ทเทมแบร์กในสตุทการ์ท
• Otterซึ่งพัฒนาขึ้นที่ห้องปฏิบัติการแห่งชาติอาร์กอนน์มีพื้นฐานมาจากความละเอียดลำดับที่หนึ่งและการปรับพารามิเตอร์ ต่อมา Otter ได้ถูกแทนที่ด้วยProver9ซึ่งทำงานร่วมกับMace4
• SETHEOเป็นระบบประสิทธิภาพสูงที่ใช้ แคลคูลัส การกำจัดแบบจำลอง ที่มุ่งเน้นเป้าหมาย ซึ่งพัฒนาขึ้นครั้งแรกโดยทีมงานภายใต้การกำกับดูแลของWolfgang Bibel E และ SETHEO ได้ถูกนำมารวมกัน (กับระบบอื่นๆ) ในตัวพิสูจน์ทฤษฎีบทแบบผสม E-SETHEO
• Vampireได้รับการพัฒนาและใช้งานครั้งแรกที่มหาวิทยาลัยแมนเชสเตอร์โดยAndrei Voronkovและ Kryštof Hoder ปัจจุบันได้รับการพัฒนาโดยทีมงานนานาชาติที่กำลังเติบโต และได้รับรางวัลชนะเลิศในประเภท FOF (และประเภทอื่นๆ) ในการแข่งขัน CADE ATP System Competition อย่างสม่ำเสมอตั้งแต่ปี 2001 ^{[ 32 ]}
• Waldmeister เป็นระบบเฉพาะทางสำหรับตรรกะลำดับที่หนึ่งแบบสมการหน่วย ซึ่งพัฒนาโดย Arnim Buch และ Thomas Hillenbrand โดยได้รับรางวัลชนะเลิศในสาขา CASC UEQ ติดต่อกันถึงสิบสี่ปี (1997–2010)
• SPASSเป็นโปรแกรมพิสูจน์ทฤษฎีบทเชิงตรรกะลำดับที่หนึ่งที่มีคุณสมบัติความเท่าเทียมกัน โปรแกรมนี้ได้รับการพัฒนาโดยกลุ่มวิจัย Automation of Logic สถาบันวิทยาศาสตร์คอมพิวเตอร์แม็กซ์พลังค์

พิพิธภัณฑ์ Theorem Prover ^{[ 33 ]}เป็นโครงการริเริ่มเพื่ออนุรักษ์แหล่งที่มาของระบบพิสูจน์ทฤษฎีบทสำหรับการวิเคราะห์ในอนาคต เนื่องจากเป็นสิ่งประดิษฐ์ทางวัฒนธรรม/วิทยาศาสตร์ที่สำคัญ พิพิธภัณฑ์แห่งนี้มีแหล่งที่มาของระบบต่างๆ มากมายที่กล่าวถึงข้างต้น

• การแก้ปัญหาอันดับแรกด้วยการรวม
• การกำจัดแบบจำลอง
• วิธีการของตารางวิเคราะห์
• การซ้อนทับและการเขียน เทอมใหม่
• การตรวจสอบแบบจำลอง
• การเหนี่ยวนำทางคณิตศาสตร์^{[ 34 ]}
• แผนภาพการตัดสินใจแบบไบนารี
• DPLL
• การรวมกันในลำดับที่สูงขึ้น
• การกำจัดตัวบ่งปริมาณ^{[ 35 ]}
• แบบจำลองภาษาขนาดใหญ่^{[ 36 ]}

• อัลท์-เออร์โก
• ออโตมาธ
• ซีวีซี
• อี
• ไอซาแพลนเนอร์
• แอลซีเอฟ
• มิซาร์
• นูพีอาร์แอล
• ความขัดแย้ง
• โปรเวอร์9
• พีวีเอส
• SPARK (ภาษาโปรแกรม)
• สิบสอง
• เครื่องพิสูจน์ทฤษฎีบท Z3

• คารีน
• Wolfram Mathematica
• วงจรวิจัย

• รายชื่อเครื่องมือพิสูจน์ทฤษฎีบท