(Selected, Linear, Definite) Linear resolution with a selection function for definite sentences.
A definite sentence has exactly one positive literal in each
clause and this literal is selected to be resolved upon,
i.e. replaced in the
goal clause by the
conjunction of
negative literals which form the body of the clause.