โปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติIsabelle ^{[ a ]} เป็นโปรแกรมพิสูจน์ทฤษฎีบทตรรกะลำดับสูง (HOL)ที่เขียนด้วยภาษา Standard MLและScalaในฐานะ โปรแกรมพิสูจน์ทฤษฎีบทสไตล์ Logic for Computable Functions (LCF) มันใช้แกนตรรกะขนาดเล็ก (เคอร์เนล) เพื่อเพิ่มความน่าเชื่อถือของการพิสูจน์โดยไม่จำเป็นต้องใช้ แต่ยังคงรองรับออบเจ็กต์การพิสูจน์ที่ชัดเจน

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

อิซาเบลล์ได้รับการตั้งชื่อโดยลอว์เรนซ์ พอลสันตามชื่อลูกสาวของเจอราร์ด ฮูเอต์^{[ 3 ]}

โปรแกรมพิสูจน์ทฤษฎีบทอิซาเบลล์เป็นซอฟต์แวร์ฟรีเผยแพร่ภายใต้ใบอนุญาต BSDฉบับ ปรับปรุง

Isabelle เป็นภาษาโปรแกรมแบบทั่วไป: มันให้เมตาตรรกะ ( ทฤษฎีประเภทแบบ อ่อน ) ซึ่งใช้ในการเข้ารหัสตรรกะเชิงวัตถุ เช่นตรรกะอันดับหนึ่ง (FOL) ตรรกะอันดับสูง (HOL) หรือทฤษฎีเซต Zermelo–Fraenkel (ZFC) ตรรกะเชิงวัตถุที่ใช้กันอย่างแพร่หลายที่สุดคือ Isabelle/HOL แม้ว่าการพัฒนาทฤษฎีเซตที่สำคัญจะเสร็จสมบูรณ์ใน Isabelle/ZF ก็ตาม วิธีการพิสูจน์หลักของ Isabelle คือเวอร์ชันอันดับสูงของresolution ซึ่งอิงจาก การรวมอันดับสูง

แม้จะเป็นแบบโต้ตอบ แต่ Isabelle ก็มีเครื่องมือการให้เหตุผลอัตโนมัติที่มีประสิทธิภาพ เช่น เครื่องมือ เขียนเทอมใหม่และตัวพิสูจน์ตารางขั้นตอนการตัดสินใจต่างๆ และผ่านทางอินเทอร์เฟซการพิสูจน์อัตโนมัติSledgehammer ตัวแก้ ปัญหาความสามารถในการทำให้เป็นจริงภายนอกโมดูลทฤษฎี (SMT) (รวมถึงCVC4 ) และตัวพิสูจน์ทฤษฎีบทอัตโนมัติแบบอิงความละเอียด (ATP) รวมถึงE , SPASSและVampire ( วิธีการพิสูจน์ Metis ^{[ b ]}สร้างการพิสูจน์ความละเอียดที่สร้างโดย ATP เหล่านี้ขึ้นใหม่) ^{[ 4 ]}นอกจากนี้ยังมี ตัวค้นหา แบบจำลอง สองตัว ( ตัว สร้างตัวอย่างค้าน ): Nitpick ^{[ 5 ]}และNunchaku ^{[ 6 ]}

Isabelle มีโลเคิลซึ่งเป็นโมดูลที่จัดโครงสร้างการพิสูจน์ขนาดใหญ่ โลเคิลจะกำหนดประเภท ค่าคงที่ และสมมติฐานภายในขอบเขตที่กำหนด^{[ 5 ]}เพื่อไม่ให้ต้องทำซ้ำสำหรับเลมมาทุก ตัว

Isar (" การให้เหตุผลกึ่งอัตโนมัติที่เข้าใจได้ ") เป็นภาษาการพิสูจน์อย่างเป็นทางการของ Isabelle ซึ่งได้รับแรงบันดาลใจจากระบบMizar ^{[ 5 ]}

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

ในทางกลับกัน การพิสูจน์แบบประกาศ (ซึ่งได้รับการสนับสนุนโดยภาษาพิสูจน์ของอิซาเบลล์ Isar) จะระบุการดำเนินการทางคณิตศาสตร์ที่ต้องดำเนินการจริง ๆ ดังนั้นจึงอ่านและตรวจสอบได้ง่ายกว่าสำหรับมนุษย์

ตัวอย่างเช่น การพิสูจน์โดยการขัดแย้งในภาษาอิสาร์ที่ระบุว่ารากที่สองของสองไม่ใช่จำนวนตรรกยะสามารถเขียนได้ดังนี้

ทฤษฎีบท sqrt2_not_rational: "sqrt 2 ∉ ℚ" พิสูจน์ให้ ?x = "sqrt 2" สมมติว่า"?x ∈ ℚ" แล้วจะได้ mn :: nat โดยที่ sqrt_rat: "¦?x¦ = m / n" และ lowest_terms: "coprime m n" โดย (rule Rats_abs_nat_div_natE) ดังนั้น"m^2 = ?x^2 * n^2" โดย (auto simp add: power2_eq_square) ดังนั้นสมการ: "m^2 = 2 * n^2" โดยใช้ of_nat_eq_iff power2_eq_square โดย fastforce ดังนั้น"2 dvd m^2" โดย simp ดังนั้น"2 dvd m" โดย simp มี"2 dvd n" พิสูจน์ - จาก‹2 dvd m› ได้ k โดยที่"m = 2 * k" .. ด้วยสมการมี"2 * n^2 = 2^2 * k^2" โดยใช้ simp ดังนั้น"2 dvd n^2" โดยใช้ simp ดังนั้น"2 dvd n" โดยใช้ simp พิสูจน์แล้วด้วย‹2 dvd m› มี"2 dvd gcd m n" โดยใช้ (rule gcd_greatest) ด้วย lowest_terms มี"2 dvd 1" โดยใช้ simp ดังนั้นเท็จ โดย ใช้ odd_one โดย ใช้ blast พิสูจน์แล้ว

Isabelle ถูกนำมาใช้เพื่อช่วยสนับสนุนวิธีการที่เป็นทางการสำหรับการกำหนดคุณสมบัติ การพัฒนา และการตรวจสอบระบบซอฟต์แวร์และฮาร์ดแวร์

Isabelle ถูกนำมาใช้เพื่อสร้างทฤษฎีบทจำนวนมากจากคณิตศาสตร์และวิทยาศาสตร์คอมพิวเตอร์อย่างเป็นทางการ เช่นทฤษฎีบทความสมบูรณ์ของ Gödelทฤษฎีบทของ Gödel เกี่ยวกับความสอดคล้องของสัจพจน์ของการเลือก ทฤษฎีบท จำนวนเฉพาะความถูกต้องของโปรโตคอลความปลอดภัยและคุณสมบัติของความหมายของภาษาโปรแกรมหลักฐานอย่างเป็นทางการจำนวนมากได้รับการเก็บรักษาไว้ในคลังหลักฐานอย่างเป็นทางการ ซึ่ง (ณ ปี 2019) มีบทความอย่างน้อย 500 บทความพร้อมหลักฐานมากกว่า 2 ล้านบรรทัด^{[ 8 ]}

• ในปี 2552 โครงการ L4.verified ที่NICTAได้สร้างหลักฐานอย่างเป็นทางการครั้งแรกเกี่ยวกับความถูกต้องในการทำงานของเคอร์เนลระบบปฏิบัติการอเนกประสงค์: ^{[ 9 ]}ไมโครเคอร์เนล seL4 (secure embedded L4 ) หลักฐานนี้ถูกสร้างและตรวจสอบใน Isabelle/HOL และประกอบด้วยสคริปต์หลักฐานมากกว่า 200,000 บรรทัดเพื่อตรวจสอบโค้ด C จำนวน 7,500 บรรทัด การตรวจสอบครอบคลุมโค้ด การออกแบบ และการใช้งาน และทฤษฎีบทหลักระบุว่าโค้ด C นั้นใช้งานตามข้อกำหนดอย่างเป็นทางการของเคอร์เนลได้อย่างถูกต้อง หลักฐานนี้พบข้อบกพร่อง 144 รายการในโค้ด C เวอร์ชันแรกของเคอร์เนล seL4 และปัญหาประมาณ 150 รายการในแต่ละด้านของการออกแบบและข้อกำหนด

• นิยามของภาษาการเขียนโปรแกรมLightweight Javaได้รับการพิสูจน์แล้วว่าถูกต้องตามประเภทใน Isabelle ^{[ 10 ]}

มีหลายภาษาและระบบที่ให้ฟังก์ชันการทำงานที่คล้ายคลึงกัน:

• Agdaเขียนด้วยภาษา Haskell
• Rocq (เดิมชื่อCoq ) เขียนด้วยภาษาOCaml
• Leanเขียนด้วยภาษา Lean และC++
• LEGOเขียนด้วยตัวอักษรมาตรฐาน ML ของรัฐนิวเจอร์ซีย์
• ระบบ Mizarที่เขียนด้วยภาษา Free Pascal
• Metamathเขียนด้วยภาษาANSI C
• Prover9เขียนด้วยภาษา Cโดยมีส่วนติดต่อผู้ใช้แบบกราฟิก (GUI) เขียนด้วยภาษา Python
• สิบสองเขียนด้วยภาษา ML มาตรฐาน

• เว็บไซต์อย่างเป็นทางการ
• อิซาเบลล์บน Stack Overflow
• คลังเอกสารพิสูจน์อักษรอย่างเป็นทางการ
• อิสาร์มาธลิบ