การกำจัดแบบจำลอง (Model elimination) เป็นชื่อที่ใช้เรียก วิธีการพิสูจน์สอง วิธี ที่คิดค้นโดยDonald W. Lovelandซึ่งวิธีแรกได้รับการตีพิมพ์ในปี 1968 ในวารสาร Journal of the ACMจุดประสงค์หลักของวิธีการนี้คือการพิสูจน์ทฤษฎีบทโดยอัตโนมัติแม้ว่าจะสามารถขยายไปสู่การเขียนโปรแกรมเชิงตรรกะ ได้อย่างง่ายดาย รวมถึง การเขียนโปรแกรมเชิงตรรกะแบบแยกส่วน (Disjunctive Logic Programming ) ที่ทั่วไปกว่าด้วย

การกำจัดแบบจำลองมีความเกี่ยวข้องอย่างใกล้ชิดกับการแก้ปัญหาในขณะเดียวกันก็มีลักษณะเฉพาะของ วิธีการ แบบตาราง (tableaux method) เป็นต้นกำเนิดของ กระบวนการ แก้ปัญหา SLDที่ใช้ในภาษาการเขียนโปรแกรมเชิงตรรกะ Prolog

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