แบบจำลองและตัวอย่างค้าน
Models And Counter-Examples ( Mace ) เป็นตัวค้นหาแบบจำลอง[ 1 ]โปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติ ส่วนใหญ่พยายามทำการพิสูจน์โดยการหักล้างบนรูปแบบปกติของข้อความในปัญหาการพิสูจน์ โดยแสดงให้เห็นว่าการรวมกันของสัจพจน์และข้อสันนิษฐานที่ถูกปฏิเสธไม่สามารถเป็นจริงพร้อมกันได้ กล่าวคือไม่มีแบบจำลอง ในทางกลับกัน ตัวค้นหาแบบจำลองเช่น Mace พยายามค้นหาแบบจำลองที่ชัดเจนของชุดข้อความ หากสำเร็จ สิ่งนี้จะสอดคล้องกับตัวอย่างค้านสำหรับข้อสันนิษฐาน กล่าวคือเป็นการหักล้างทฤษฎีบท (ที่อ้าง)
Mace ได้รับอนุญาตภายใต้GNU GPL [ 2 ]
ดูเพิ่มเติม
ลิงก์ภายนอก
- การดาวน์โหลดระบบ
 | บทความเกี่ยวกับตรรกศาสตร์นี้ ยัง ไม่สมบูรณ์คุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป |