HOL ( Higher Order Logic ) หมายถึงตระกูลของระบบพิสูจน์ทฤษฎีบทแบบโต้ตอบที่ใช้ ตรรกะ (ลำดับสูง)และกลยุทธ์การใช้งานที่คล้ายคลึงกัน ระบบในตระกูลนี้ปฏิบัติตาม แนวทาง LCF (Logic for Computable Functions) เนื่องจากถูกนำไปใช้ในรูปแบบไลบรารีซึ่งกำหนดชนิดข้อมูลนามธรรมของทฤษฎีบท ที่ได้รับการพิสูจน์ แล้ว โดยที่วัตถุใหม่ของชนิดนี้สามารถสร้างขึ้นได้โดยใช้ฟังก์ชันในไลบรารีเท่านั้น ซึ่งสอดคล้องกับกฎการอนุมานในตรรกะลำดับสูง ตราบใดที่ฟังก์ชันเหล่านี้ถูกนำไปใช้อย่างถูกต้อง ทฤษฎีบททั้งหมดที่ได้รับการพิสูจน์ในระบบจะต้องถูกต้อง ด้วยเหตุนี้ ระบบขนาดใหญ่จึงสามารถสร้างขึ้นบนแกนหลักขนาดเล็กที่เชื่อถือได้

ระบบในตระกูล HOL ใช้MLหรือเวอร์ชันที่พัฒนาต่อยอดจาก ML โดย ML ถูกพัฒนาขึ้นพร้อมกับ LCF ในฐานะภาษาเมตาสำหรับระบบพิสูจน์ทฤษฎีบท ซึ่งชื่อนี้ย่อมาจาก "Meta-Language" (ภาษาเมตา)

ระบบ HOL ใช้รูปแบบต่างๆ ของตรรกะลำดับสูงแบบคลาสสิก ซึ่งมีพื้นฐานเชิงสัจพจน์ที่เรียบง่าย มีสัจพจน์น้อย และความหมายที่เข้าใจได้ดี^{[ 1 ]}

ตรรกะที่ใช้ในตัวพิสูจน์ HOL เกี่ยวข้องอย่างใกล้ชิดกับ Isabelle/HOL ^{[ 2 ]} ซึ่ง เป็น ตรรกะที่ใช้กันอย่างแพร่หลายที่สุดของIsabelle

ระบบ HOL จำนวนหนึ่ง (ซึ่งใช้ตรรกะพื้นฐานเดียวกัน) ยังคงใช้งานได้อยู่:

1. HOL4 — ระบบเดียวที่ยังคงได้รับการบำรุงรักษาและพัฒนาในปัจจุบันซึ่งสืบเนื่องมาจากระบบ HOL88 ซึ่งเป็นจุดสูงสุดของความพยายามในการใช้งาน HOL ดั้งเดิม นำโดยMike Gordon HOL88 มี การใช้งาน ML ของตัวเอง ซึ่งถูกนำไปใช้บนCommon Lispระบบที่ตามมาหลังจาก HOL88 (HOL90, hol98 และ HOL4) ทั้งหมดถูกนำไปใช้ในStandard MLในขณะที่ hol98 เชื่อมโยงกับMoscow ML HOL4 สามารถสร้างได้โดยใช้ Moscow ML หรือPoly/ML ก็ได้ ทั้งหมดมาพร้อมกับไลบรารีขนาดใหญ่ของโค้ดพิสูจน์ทฤษฎีบทซึ่งใช้ระบบอัตโนมัติเพิ่มเติมบนโค้ดหลักที่เรียบง่ายมาก HOL4 ได้รับอนุญาตภายใต้ BSD ^{[ 3 ]}
2. HOL Light — เวอร์ชัน "มินิมอลลิสต์" เชิงทดลองของ HOL ซึ่งต่อมาได้พัฒนาเป็น HOL เวอร์ชันหลักอีกแบบหนึ่ง รากฐานเชิงตรรกะของมันยังคงเรียบง่ายอย่างผิดปกติ HOL Light ซึ่งเดิมทีเขียนด้วยCaml Lightปัจจุบันใช้OCaml HOL Light มีให้ใช้งานภายใต้ใบอนุญาต BSD ใหม่^{[ 4 ]}
3. ProofPower — ชุดเครื่องมือหกอย่างที่ออกแบบมาเพื่อสนับสนุนการทำงานกับสัญลักษณ์ Zสำหรับการกำหนดคุณสมบัติอย่างเป็นทางการ โดยใช้พื้นฐานจาก HOL เครื่องมือ PPDaz ที่สนับสนุนการกำหนดคุณสมบัติและการตรวจสอบโปรแกรมที่เขียนด้วยภาษา Ada บางส่วนนั้น ก่อนหน้านี้มีให้ใช้งานภายใต้ใบอนุญาตกรรมสิทธิ์เท่านั้น ขณะนี้เครื่องมือทั้งหมดมีให้ใช้งานภายใต้ใบอนุญาต GNU GPL v2 แล้ว
4. HOL Zero — การใช้งานแบบเรียบง่ายที่เน้นความน่าเชื่อถือ HOL Zero ได้รับอนุญาตภายใต้ GNU GPL 3+ ^{[ 5 ]}
5. Candle — การใช้งาน HOL Light ที่ได้รับการตรวจสอบแบบครบวงจรบน CakeML ^{[ 6 ]}

โครงการCakeMLได้พัฒนาคอมไพเลอร์ที่ได้รับการพิสูจน์อย่างเป็นทางการสำหรับ ML ^{[ 7 ]}ก่อนหน้านี้ HOL ถูกใช้เพื่อพัฒนาการ ใช้งาน Lisp ที่ได้รับการพิสูจน์อย่างเป็นทางการ ซึ่งทำงานบน ARM, x86 และ PowerPC ^{[ 8 ]}

นอกจากนี้ HOL ยังถูกใช้เพื่อกำหนดความหมายของมัลติโปรเซสเซอร์ x86 อย่างเป็นทางการ ^{[ 9 ]}รวมถึงรหัสเครื่องสำหรับสถาปัตยกรรมPower ISAและARM ^{[ 10 ]}

• กอร์ดอน, ไมเคิล เจซี (1996). "จาก LCF ถึง HOL: ประวัติย่อ" . สืบค้นเมื่อ2007-10-11 .

• เว็บไซต์อย่างเป็นทางการ
• เอกสารที่ระบุตรรกะพื้นฐานของ HOL
• คู่มือรายละเอียด HOL4รวมถึงข้อกำหนดตรรกะของระบบ
• ข้อมูลห้องสมุดเสมือนจริงเกี่ยวกับวิธีการเชิงทางการ