U radu se opisuje uređena linearna rezolucija sa markiranim literalima i njene specifičnosti. Da bi se očuvala potpunost metode izvršena je modifikacija algoritma za određivanje rezolvente. Na bazi modifikovane uređene linearne rezolucije sa markiranim literalima izgrađen je sistem za automatsko dokazivanje teorema. Sistem je implementiran na PC - računani i dopušta varijabilne strategije pretraživanja. Pretpostavke i tvrđenja koje treba dokazati, zapisuju se odgovarajućim formulama predikatskog računa prvog reda. U radu se daje opis implementiranog sistema za automatsko dokazivanje teorema, prikazuju se njegove karakteristike i oblasti primene. Posebno se razmatra odnos ovakvog automatskog dokazivača teorema i Prolog-a.