Eliminacja modelu

Model Elimination to nazwa pary procedur dowodowych wymyślonych przez Donalda W. Lovelanda , z których pierwsza została opublikowana w 1968 roku w Journal of the ACM. Ich głównym celem jest przeprowadzanie zautomatyzowanego dowodzenia twierdzeń , chociaż można je łatwo rozszerzyć na programowanie w logice , w tym bardziej ogólne programowanie w logice dysjunkcyjnej .

Eliminacja modelu jest ściśle związana z rozdzielczością , a jednocześnie nosi cechy metody Tableaux . Jest protoplastą rozwiązywania SLD używanej w języku programowania logiki Prolog .

Chociaż nieco przyćmiona uwagą i postępem w dowodach twierdzeń o rozdzielczości, eliminacja modelu nadal przyciąga uwagę badaczy i twórców oprogramowania. Obecnie aktywnie rozwija się kilka narzędzi do dowodzenia twierdzeń, które są oparte na procedurze eliminacji modelu.