การสมมติเชิงธีตา (θ-subsumption หรือเรียกสั้น ๆ ว่า subsumption) เป็น ความสัมพันธ์ ที่ตัดสินได้ระหว่างประโยคย่อยลำดับที่หนึ่ง สองประโยค ซึ่งรับประกันว่าประโยคย่อยหนึ่งบ่งชี้อีกประโยคย่อยหนึ่งในเชิงตรรกะ แนวคิดนี้ได้รับการแนะนำครั้งแรกโดยJohn Alan Robinsonในปี 1965 และได้กลายเป็นแนวคิดพื้นฐานในการเขียนโปรแกรมเชิงตรรกะแบบอุปนัยการตัดสินใจว่าประโยคย่อยที่กำหนดให้สมมติเชิงธีตากับอีกประโยคย่อยหนึ่งหรือไม่นั้น เป็นปัญหา NP-complete

ประโยคย่อย ซึ่งก็คือการเชื่อมประโยคย่อยแบบ " หรือ" ของ ตัวแปรเชิงตรรกะลำดับที่หนึ่งสามารถพิจารณาได้ว่าเป็นเซตที่ประกอบด้วยตัวแปรย่อยแบบ "หรือ" ทั้งหมดของมัน

ตามธรรมเนียมนี้ อนุประโยคθ-subsume อนุประโยคหนึ่งหากมีการแทนที่ซึ่งอนุประโยคที่ได้จากการใช้กับเป็นเซตย่อยของ^{[ 1 ]}${\textstyle c_{1}}$${\textstyle c_{2}}$${\displaystyle \theta }$${\textstyle \theta }$${\textstyle c_{1}}$${\textstyle c_{2}}$

การครอบคลุมแบบ θ เป็นความสัมพันธ์ที่อ่อนกว่าการอนุมานเชิงตรรกะกล่าวคือ เมื่อใดก็ตามที่ประโยคหนึ่งครอบคลุมประโยคอื่นแบบ θ แล้ว ประโยคนั้นก็จะอนุมานประโยคอื่นนั้น ได้ในเชิงตรรกะเช่นกัน อย่างไรก็ตาม ข้อความกลับกันนั้นไม่เป็นจริง กล่าวคือ ประโยคหนึ่งสามารถอนุมานประโยคอื่นได้ในเชิงตรรกะ แต่ไม่สามารถครอบคลุมประโยคอื่นแบบ θ ได้ ${\textstyle c_{1}}$${\textstyle c_{2}}$${\textstyle c_{1}}$${\textstyle c_{2}}$

การครอบคลุมแบบ θ สามารถตัดสินได้ กล่าวคือ ปัญหาที่ว่าประโยคหนึ่งครอบคลุมประโยคอื่นแบบ θ หรือไม่นั้น เป็นปัญหา NP-complete ตามความยาวของประโยค ซึ่งยังคงเป็นเช่นนั้นเมื่อจำกัดการตั้งค่าไว้ที่คู่ของประโยคHorn ^{[ 2 ]}

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

θ-subsumption ถูกนำเสนอครั้งแรกโดยJ. Alan Robinsonในปี 1965 ในบริบทของresolution [ ^{4 ]}และถูกนำไปใช้กับการเขียนโปรแกรมตรรกะแบบอุปนัยครั้งแรกโดย^Gordon Plotkinในปี 1970 เพื่อค้นหาและลดความทั่วไปน้อยที่สุดของเซตของข้อความ^{[ 5 ]}ในปี 1977 Lewis D. Baxter พิสูจน์ว่า θ-subsumption เป็นปัญหา NP-complete ^{[ 6 ]}และงานสำคัญในปี 1979 เกี่ยวกับปัญหา NP-complete เรื่องComputers and Intractabilityได้รวม θ-subsumption ไว้ในรายการปัญหา NP-complete ด้วย^{[ 2 ]}

โปรแกรมพิสูจน์ ทฤษฎีบท ที่ใช้ แคลคูลัส การแก้ปัญหาหรือการซ้อนทับจะใช้ θ-subsumption เพื่อตัดข้อความที่ซ้ำซ้อนออก^{[ 7 ]}นอกจากนี้ θ-subsumption ยังเป็นแนวคิดที่โดดเด่นที่สุดของการอนุมานที่ใช้ในการเขียนโปรแกรมตรรกะแบบอุปนัยซึ่งเป็นเครื่องมือพื้นฐานในการพิจารณาว่าข้อความหนึ่งเป็นการเฉพาะหรือการทั่วไปของอีกข้อความหนึ่งหรือไม่^{[ 1 ]} นอกจากนี้ยังใช้เพื่อทดสอบว่าข้อความครอบคลุมตัวอย่างหรือไม่ และเพื่อพิจารณาว่าข้อความสองข้อความที่กำหนดให้ซ้ำซ้อนหรือไม่^{[ 2 ]}