모델 제거

Model elimination

모델 제거(Model Removaling)는 도널드 W. 러브랜드가 발명한 증명 절차 쌍에 붙이는 명칭으로, 그 중 첫 번째는 1968년 ACM 저널에 실렸다.이들의 1차적인 목적은 보다 일반적인 이분법 논리 프로그래밍을 포함하여 로직 프로그래밍으로 쉽게 확장될 수 있지만 자동화된 정리 검증을 수행하는 것이다.

모델 제거는 분해능과 밀접하게 관련되어 있는 동시에 Tableaux 방법의 특성을 가지고 있다.Prolog 논리 프로그래밍 언어에 사용되는 SLD 분해능 절차의 시조다.

분해능을 추구하는 사람들에 대한 관심과 진행에 다소 주춤하는 동안, 모델 제거는 연구자들과 소프트웨어 개발자들의 관심을 계속 끌어왔다.오늘날에는 모델 제거 절차에 근거한 몇 가지 정리가 활발히 전개되고 있다.

참조