Logic for Computable Functions ( LCF ) เป็นโปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติแบบ โต้ตอบ ที่พัฒนาขึ้นที่มหาวิทยาลัยสแตนฟอร์ดและเอดินบะระโดยRobin Milnerและผู้ร่วมงานในช่วงต้นทศวรรษ 1970 โดยอิงจากพื้นฐานทางทฤษฎีของตรรกะของฟังก์ชันที่คำนวณได้ซึ่งเสนอโดยDana Scott ก่อนหน้านี้ การทำงานในระบบ LCF ได้นำภาษาโปรแกรม อเนกประสงค์ ML มา ใช้เพื่อให้ผู้ใช้สามารถเขียนกลยุทธ์การพิสูจน์ทฤษฎีบท โดยรองรับชนิดข้อมูลเชิงพีชคณิต พหุรูปเชิงพารามิเตอร์ชนิดข้อมูลนามธรรมและข้อ ยกเว้น

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

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

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

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

หนึ่งในระบบที่พัฒนาต่อมาคือ Cambridge LCF ระบบรุ่นหลังๆ ได้ลดความซับซ้อนของตรรกะโดยใช้ฟังก์ชันทั้งหมดแทนฟังก์ชันบางส่วน ทำให้เกิดHOL , HOL Lightและโปรแกรมช่วยพิสูจน์ Isabelleที่รองรับตรรกะต่างๆ ณ ปี 2019 โปรแกรมช่วยพิสูจน์ Isabelle ยังคงมีการใช้งานตรรกะ LCF อยู่ นั่นคือ Isabelle/LCF