E เป็น ตัวพิสูจน์ทฤษฎีบทประสิทธิภาพสูงสำหรับตรรกะลำดับแรกแบบเต็มรูปแบบที่มีความเท่าเทียมกัน^{[ 1 ]}โดยอิงจากแคลคูลัสการซ้อนทับ เชิงสมการ และใช้กระบวนทัศน์เชิงสมการล้วนๆ ได้รับการบูรณาการเข้ากับตัวพิสูจน์ทฤษฎีบทอื่นๆ และอยู่ในกลุ่มระบบที่ดีที่สุดในการแข่งขันการพิสูจน์ทฤษฎีบทหลายรายการ E ได้รับการพัฒนาโดย Stephan Schulz ซึ่งเดิมอยู่ในกลุ่มการให้เหตุผลอัตโนมัติที่TU Munichปัจจุบันอยู่ที่มหาวิทยาลัยรัฐสหกรณ์ Baden-Württemberg Stuttgart

ระบบนี้ใช้แคลคูลัสการซ้อนทับ สมการเป็น พื้นฐาน แตกต่างจากโปรแกรมพิสูจน์อื่นๆ ส่วนใหญ่ในปัจจุบัน การใช้งานจริงใช้กระบวนทัศน์สมการล้วนๆ และจำลองการอนุมานที่ไม่ใช่สมการผ่านการอนุมานความเท่าเทียมกันที่เหมาะสม นวัตกรรมที่สำคัญ ได้แก่ การเขียนเทอมใหม่ร่วมกัน (ซึ่งการลดรูปสมการที่เป็นไปได้หลายอย่างจะดำเนินการในขั้นตอนเดียว) ^{[ 2 ]} โครงสร้างข้อมูล การจัดทำดัชนีเทอมที่มีประสิทธิภาพหลายอย่างเพื่อเร่งความเร็วในการอนุมาน กลยุทธ์การเลือกตัวอักษรการอนุมานขั้นสูง และการใช้ เทคนิค การเรียนรู้ของเครื่อง ต่างๆ เพื่อปรับปรุงพฤติกรรมการค้นหา^{[ 2 ] [ 3 ] [ 4 ]}ตั้งแต่เวอร์ชัน 2.0 E รองรับ ตรรกะแบบ เรียงลำดับหลายแบบ^{[ 5 ]}

E ถูกนำไปใช้ในCและพกพาได้ไปยังUNIXรุ่นต่างๆ ส่วนใหญ่และ สภาพแวดล้อม Cygwinมีให้ใช้งานภายใต้GNU GPL ^{[ 6 ]}

ระบบพิสูจน์นี้ทำงานได้ดีอย่างต่อเนื่องในการแข่งขันระบบ CADE ATPโดยชนะในประเภท CNF/MIX ในปี 2000 และติดอันดับระบบชั้นนำมาโดยตลอด^{[ 7 ]}ในปี 2008 ได้อันดับสอง^{[ 8 ]}ในปี 2009 ได้รับรางวัลรองชนะเลิศอันดับสองในประเภท FOF (ตรรกะลำดับแรกแบบสมบูรณ์) และ UEQ ( ตรรกะสมการ หน่วย ) และอันดับสาม (หลังจากVampire สองเวอร์ชัน ) ในประเภท CNF (ตรรกะแบบข้อความ) ^{[ 9 ]}ระบบนี้ทำผลงานได้ดีซ้ำในประเภท FOF และ CNF ในปี 2010 และได้รับรางวัลพิเศษในฐานะระบบ "ดีที่สุดโดยรวม" ^{[ 10 ]}ในการแข่งขัน CASC-23 E ปี 2011 ชนะในประเภท CNF และได้อันดับสองใน UEQ และ LTB ^{[ 11 ]}

E ได้รับการบูรณาการเข้ากับโปรแกรมพิสูจน์ทฤษฎีบทอื่นๆ อีกหลายโปรแกรม โดย E ร่วมกับVampire , SPASS , CVC4และZ3เป็นแกนหลักของกลยุทธ์SledgehammerของIsabelle ^{[ 12 ] [ 13 ]}นอกจากนี้ E ยังเป็นกลไกการให้เหตุผลใน SInE ^{[ 14 ]}และ LEO-II ^{[ 15 ]}และใช้เป็นระบบการสร้างประโยคสำหรับ iProver ^{[ 16 ]}

การประยุกต์ใช้ E รวมถึงการให้เหตุผลบนออนโทโลยีขนาดใหญ่^{[ 17 ]} การตรวจสอบซอฟต์แวร์^{[ 18 ]}และการรับรองซอฟต์แวร์^{[ 19 ]}

• หน้าแรกของเว็บไซต์
• นักพัฒนาของ E