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.