Pogledaj metod rezolucije za predikatski račun prvog reda u nekoj knjizi o matematičkoj logici. Ako želiš nešto kraće za čitanje, možda pogledaj ovde (čas 8, 9 i 10). Na Vikipediji takođe postoji odgovarajući članak.