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.
- Loveland, DW (1968) Dowód twierdzenia mechanicznego przez eliminację modelu . Dziennik ACM, 15, 236-251.