- Selective: at each resolution step, a fixed computation rule is applied to select which atom from the goal will be resolved next
- Linear: at each resolution step, the most recently derived resolvent is used as the next goal
- Definite: all the program clauses are definite clauses