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

PhoX ได้รับการออกแบบและพัฒนาขึ้นครั้งแรกโดยChristophe Raffalliโดยใช้ภาษาโปรแกรมOCaml เขายังคงเป็นผู้นำทีมพัฒนาในปัจจุบัน ซึ่งเป็นการร่วมมือกันระหว่างมหาวิทยาลัย Savoyและมหาวิทยาลัย Paris VII

เป้าหมายหลักของโครงการ PhoX คือการสร้างโปรแกรมตรวจสอบความถูกต้องของโค้ดที่ใช้งานง่าย โดยใช้ระบบประเภทข้อมูลที่พัฒนาโดยJean-Louis Krivineจากมหาวิทยาลัยปารีส VII โปรแกรมนี้ถูกออกแบบมาให้ใช้งานง่ายกว่าระบบอื่นๆ ในขณะเดียวกันก็ยังคงความสามารถในการขยาย ประสิทธิภาพ และการแสดงออกที่ดี เมื่อเทียบกับระบบอื่นๆ ไวยากรณ์การสร้างหลักฐานถูกทำให้ง่ายขึ้นและใกล้เคียงกับภาษาธรรมชาติ คุณสมบัติอื่นๆ ได้แก่ การสร้างหลักฐานด้วย GUI การแสดงผลแบบจัดรูปแบบ และการพิสูจน์ความถูกต้องของโปรแกรมในภาษาโปรแกรม ML

ปัจจุบัน PhoX ถูกนำไปใช้ในการสอนตรรกศาสตร์ที่มหาวิทยาลัยซาวอย อยู่ในสถานะทดลองแต่สามารถใช้งานได้ และเผยแพร่ภายใต้CeCILL 2.0

• เว็บไซต์ Phox

บทความซอฟต์แวร์ทางวิทยาศาสตร์นี้ ยัง ไม่สมบูรณ์คุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี

บทความเกี่ยวกับซอฟต์แวร์โอเพนซอร์สและใช้งานได้ฟรีนี้ ยังเป็น เพียงบทความย่อคุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี