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

การทำงานหลายอย่างในโปรแกรมพิสูจน์ทฤษฎีบทอัตโนมัติจำเป็นต้องค้นหาในชุดคำและประโยคจำนวนมาก การทำงานดังกล่าวโดยทั่วไปจะอยู่ในรูปแบบต่อไปนี้: กำหนดชุดคำ (ประโยค) และคำค้นหา (ประโยค) มาให้ ค้นหาคำ ที่เกี่ยวข้องกับคำค้นหาในบางคำหรือทุกคำตามเงื่อนไขการค้นหาที่กำหนด เงื่อนไขการค้นหาที่น่าสนใจที่สุดมักถูกกำหนดในรูปแบบของการมีอยู่ของการแทนที่ซึ่งเชื่อมโยงคำค้นหาและคำที่ค้นพบในลักษณะพิเศษต่อไปนี้คือรายการเงื่อนไขการค้นหาที่ใช้บ่อยในโปรแกรมพิสูจน์ทฤษฎีบท: ${\displaystyle S}$${\displaystyle q}$${\displaystyle S}$${\displaystyle t}$${\displaystyle q}$${\displaystyle t}$

• เทอมสามารถหาค่าเท่ากับเทอม ได้กล่าวคือ มีการแทนที่ อยู่เช่นนั้น=${\displaystyle q}$${\displaystyle t}$${\displaystyle \theta }$${\displaystyle q\theta }$${\displaystyle t\theta }$
• เทอมนี้เป็นตัวอย่างของ กล่าวคือ มีการแทนที่ อยู่เช่นนั้น=${\displaystyle t}$${\displaystyle q}$${\displaystyle \theta }$${\displaystyle q\theta }$${\displaystyle t}$
• เงื่อนไขนี้เป็นการสรุปทั่วไปของ เงื่อนไข ดังกล่าว กล่าวคือมีการแทนที่เงื่อนไขหนึ่ง ที่ทำให้เงื่อนไขนั้นเป็นจริง${\displaystyle t}$${\displaystyle q}$${\displaystyle \theta }$${\displaystyle q}$${\displaystyle t\theta }$
• อนุประโยคθ ครอบคลุมอนุประโยค θ กล่าวคือ มีการแทนที่อยู่เช่นนั้นเป็นเซตย่อย/เซตย่อยหลายเซตของ${\displaystyle q}$${\displaystyle t}$${\displaystyle \theta }$${\displaystyle q\theta }$${\displaystyle t}$
• ประโยคย่อย ถูกรวม โดยθ กล่าวคือมีการแทนที่อยู่จริงโดยที่เป็นเซตย่อย/เซตย่อยหลายเซตของ${\displaystyle q}$${\displaystyle t}$${\displaystyle \theta }$${\displaystyle t\theta }$${\displaystyle q}$

โดยส่วนใหญ่แล้ว เราสนใจที่จะค้นหาคำทดแทนที่เหมาะสมอย่างชัดเจน พร้อมกับคำที่ดึงมาได้มากกว่าที่จะเพียงแค่พิสูจน์ว่ามีคำทดแทนเหล่านั้นอยู่จริง ${\displaystyle t}$

บ่อยครั้งที่ขนาดของชุดคำที่ต้องการค้นหามีขนาดใหญ่ การเรียกใช้งานเกิดขึ้นบ่อย และเงื่อนไขการค้นหาค่อนข้างซับซ้อน ในสถานการณ์เช่นนี้การค้นหาแบบเชิงเส้นใน ชุด คำ เมื่อเงื่อนไขการค้นหาถูกทดสอบกับทุกคำจากชุดคำจะมีต้นทุนสูงเกินไป เพื่อแก้ไขปัญหานี้ จึงมีการออกแบบโครงสร้างข้อมูลพิเศษที่เรียกว่าดัชนีเพื่อรองรับการค้นหาที่รวดเร็ว โครงสร้างข้อมูลดังกล่าว พร้อมด้วยอัลกอริธึมที่ใช้ในการบำรุงรักษาและการค้นหาดัชนี เรียกว่า เทคนิคการจัด ทำ ดัชนีคำ${\displaystyle S}$${\displaystyle S}$

• ต้นไม้จำแนก
• ต้นไม้ทดแทน
• การจัดทำดัชนีเส้นทาง

ต้นไม้ทดแทนมีประสิทธิภาพเหนือกว่าการจัดทำดัชนีเส้นทาง การจัดทำดัชนีต้นไม้จำแนก และต้นไม้นามธรรม^{[ 2 ]}

ดัชนีคำศัพท์ต้นไม้จำแนกจะเก็บข้อมูลไว้ในโครงสร้างข้อมูลไทร^{[ 3 ]}

การจัดทำดัชนีโดยใช้ตัวแปรแรกเป็นกลยุทธ์ที่พบได้บ่อยที่สุด โดยใช้ตัวแปรแรกเป็นดัชนี วิธีนี้ช่วยแยกแยะค่าอะตอมและฟังก์ชัน หลัก ของเทอมประกอบได้

การจัดทำดัชนีโดยไม่ใช้พารามิเตอร์แรกเป็นรูปแบบหนึ่งของการจัดทำดัชนีโดยใช้พารามิเตอร์แรก โดยใช้วิธีการเดียวกันหรือคล้ายคลึงกับการจัดทำดัชนีโดยใช้พารามิเตอร์แรกกับพารามิเตอร์ทางเลือกหนึ่งตัวหรือมากกว่านั้น ตัวอย่างเช่น หากการเรียกใช้述语ใช้ตัวแปรสำหรับพารามิเตอร์แรก ระบบอาจเลือกใช้พารามิเตอร์ที่สองเป็นดัชนีแทน

การสร้างดัชนีแบบหลายอาร์กิวเมนต์จะสร้างดัชนีรวมเหนืออาร์กิวเมนต์ที่กำหนดค่าไว้หลายรายการ หากไม่มีดัชนีอาร์กิวเมนต์เดี่ยวที่มีความเฉพาะเจาะจงเพียงพอ

การทำดัชนีเชิงลึก (Deep indexing) ใช้เมื่อประโยคย่อยหลายประโยคใช้ฟังก์ชันหลักเดียวกันสำหรับอาร์กิวเมนต์บางตัว โดยจะใช้เทคนิคการทำดัชนีแบบเดียวกันหรือคล้ายกันกับอาร์กิวเมนต์ของประโยคย่อยเหล่านั้นแบบเรียกซ้ำ

การจัดทำดัชนี Trieใช้ต้นไม้คำนำหน้าเพื่อค้นหาข้อความที่เกี่ยวข้อง^{[ 4 ]}

• P. Graf, การจัดทำดัชนีคำศัพท์, เอกสารประกอบการบรรยายวิชาวิทยาการคอมพิวเตอร์ 1053, 1996 (ภาพรวมที่อาจล้าสมัยเล็กน้อย)
• R. Sekar และ IV Ramakrishnan และ A. Voronkov, การจัดทำดัชนีคำศัพท์ ใน A. Robinson และ A. Voronkov, บรรณาธิการ, คู่มือการให้เหตุผลอัตโนมัติเล่ม 2, 2001 (ภาพรวมล่าสุด)
• WW McCune, การทดลองกับการจัดทำดัชนีต้นไม้จำแนกและการจัดทำดัชนีเส้นทางสำหรับการดึงคำศัพท์, วารสารการให้เหตุผลอัตโนมัติ, 9(2), 1992
• P. Graf, การจัดทำดัชนีต้นไม้ทดแทน, รายงานการประชุม RTA, บันทึกการบรรยายในวิทยาการคอมพิวเตอร์ 914, 1995
• M. Stickel, วิธีการจัดทำดัชนีเส้นทางสำหรับจัดทำดัชนีคำศัพท์, รายงานทางเทคนิคหมายเลข 473, ศูนย์ปัญญาประดิษฐ์ , SRI International , 1989
• S. Schulz, การรวมข้อความอย่างง่ายและมีประสิทธิภาพด้วยการจัดทำดัชนีเวกเตอร์คุณลักษณะ, รายงานการประชุมเชิงปฏิบัติการ IJCAR-2004 ESFOR, 2004
• A. Riazanov และ A. Voronkov, โครงสร้างรหัสแบบปรับตัวได้บางส่วน, ในรายงานการประชุม JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
• H. Ganzinger และ R. Nieuwenhuis และ P. Nivela, การจัดทำดัชนีคำศัพท์อย่างรวดเร็วด้วยต้นไม้บริบทที่เข้ารหัส, วารสารการให้เหตุผลอัตโนมัติ, 32(2), 2004
• A. Riazanov และ A. Voronkov, การเรียกค้นอินสแตนซ์ที่มีประสิทธิภาพด้วยการจัดทำดัชนีเส้นทางมาตรฐานและเชิงสัมพันธ์, ข้อมูลและการคำนวณ, 199(1–2), 2005