A resolução na lógica de predicados é feita de forma muito parecida com a resolução na lógica proposicional. Devemos primeiro colocar a fórmula na forma normal conjuntiva (FNC), e depois fazer os resolventes. É importante destacar que na hora de fazer os resolventes entre as cláusulas devemos aplicar uma substituição que unifique os dois literais complementares que se deseja eliminar.