ในตรรกศาสตร์ทางคณิตศาสตร์ การอนุมานเชิงลึก ( deep inference)เป็นชื่อเรียกแนวคิดทั่วไปในทฤษฎีการพิสูจน์เชิงโครงสร้าง (structural proof theory)ที่แตกต่างจากแคลคูลัสลำดับแบบคลาสสิก (classical sequent calculus)โดยการขยายแนวคิดเรื่องโครงสร้างเพื่อให้สามารถอนุมานได้ในบริบทที่มีความซับซ้อนเชิงโครงสร้างสูง คำว่าการอนุมานเชิงลึกโดยทั่วไปสงวนไว้สำหรับแคลคูลัสการพิสูจน์ที่มีความซับซ้อนเชิงโครงสร้างไม่จำกัด ในบทความนี้ เราจะใช้คำว่าการอนุมานที่ไม่ตื้น (non-shallow inference)เพื่ออ้างถึงแคลคูลัสที่มีความซับซ้อนเชิงโครงสร้างมากกว่าแคลคูลัสลำดับ แต่ไม่ถึงกับไม่จำกัด แม้ว่าในปัจจุบันจะยังไม่ใช่ศัพท์ที่ได้รับการยอมรับอย่างเป็นทางการก็ตาม

การอนุมานเชิงลึกไม่สำคัญในตรรกศาสตร์นอกเหนือจากทฤษฎีการพิสูจน์เชิงโครงสร้าง เนื่องจากปรากฏการณ์ที่นำไปสู่การเสนอ ระบบที่เป็นทางการที่มีการอนุมานเชิงลึกล้วนเกี่ยวข้องกับทฤษฎีบทการกำจัดการตัดแคลคูลัสแรกของการอนุมานเชิงลึกได้รับการเสนอโดยKurt Schütte [ ^{1 ] แต่}แนวคิดนี้ไม่ได้รับความสนใจมากนักในขณะนั้น

นูเอล เบลแนปเสนอตรรกศาสตร์แสดงผล (display logic)เพื่อพยายามอธิบายแก่นแท้ของทฤษฎีการ พิสูจน์เชิงโครงสร้าง แคลคูลัสของโครงสร้าง (calculus of structures)ถูกเสนอขึ้นเพื่ออธิบาย ตรรกศาสตร์ไม่สลับที่ (noncommutative logic) โดยปราศจากการตัด (cut-free ) แคลคูลัสแบบวนรอบ (circquent calculus ) ถูกพัฒนาขึ้นเป็นระบบการอนุมานเชิงลึกที่ช่วยให้สามารถอธิบายความเป็นไปได้ของการแบ่งปันส่วนประกอบย่อยได้อย่างชัดเจน

• Kai Brünnler, "Deep Inference and Symmetry in Classical Proofs" ( วิทยานิพนธ์ปริญญาเอก ปี 2004 เก็บถาวรเมื่อ 2006-12-08 ที่Wayback Machine ) ตีพิมพ์เป็นหนังสือโดยสำนักพิมพ์ Logos Verlag ( ISBN) 978-3-8325-0448-9)
• การอนุมานเชิงลึกและแคลคูลัสของโครงสร้างบทนำและหน้าเว็บอ้างอิงเกี่ยวกับงานวิจัยที่กำลังดำเนินอยู่ในการอนุมานเชิงลึก
• Aler Tubella, Andrea; Straßburger, Lutz (2019). บทนำสู่การอนุมานเชิงลึก: เอกสารประกอบการบรรยายสำหรับ ESSLLI'19, 5–16 สิงหาคม 2019, มหาวิทยาลัยลัตเวีย(PDF) (รายงาน)

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

• วี
• ที
• อี