An alternative inference technique that is sound and complete (unlike forward and backward reasoning only being sound). Unfortunately, inference systems based on resolution are far more computationally expensive.