Jape เป็นโปรแกรม ช่วยพิสูจน์แบบกราฟิกที่ปรับแต่งได้ซึ่งเดิมพัฒนาโดยRichard Bornatที่Queen Mary, University of LondonและBernard Sufrinที่มหาวิทยาลัยOxford ^{[ 2 ]}โปรแกรมนี้สามารถใช้งานได้บน ระบบปฏิบัติการ Mac , UnixและWindowsเขียนด้วย ภาษาโปรแกรม Javaและเผยแพร่ภายใต้GNU GPL

มีการอ้างว่า Jape เป็นโปรแกรมที่ได้รับความนิยมมากที่สุดสำหรับ "การสอนตรรกะโดยใช้คอมพิวเตอร์ช่วย" ซึ่งเกี่ยวข้องกับแบบฝึกหัดในการพัฒนาการพิสูจน์ในตรรกะทางคณิตศาสตร์^{[ 3 ]}

Jape ถูกสร้างขึ้นในปี 1992 โดย Richard Bornat และ Bernard Sufrin โดยมีจุดประสงค์เพื่อให้เข้าใจการให้เหตุผลเชิงรูปแบบได้ดียิ่งขึ้น Bernard Sufrin เป็นผู้ตั้งชื่อว่า "Jape" ^{[ 2 ]}

ในปี 2019 พวกเขาได้เผยแพร่โค้ดบน GitHub ^{[ 4 ]}

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

Jape ทำงานร่วมกับแคลคูลัสลำดับและอนุมานธรรมชาติ แบบต่างๆ นอกจากนี้ยังรองรับการพิสูจน์อย่างเป็นทางการด้วยตัวบ่งปริมาณ [ ^{2 ] : 84}

• รายชื่อผู้ช่วยพิสูจน์อักษร

• เว็บไซต์จัดจำหน่ายอย่างเป็นทางการของ Jape Online
• พอร์ทัลJape SourceForge
• Jape บน Github