Index Conditions of Resolution

In this paper, the following results are proved: (1) Using both deletion strategy and lock strategy, resolution is complete for a clause set where literals with the same predicate or proposition symbol have the same index. (2) Using deletion strategy, both positive unit lock resolution and input lock resolution are complete for a Horn set where the indexes of positive literals are greater than those of negative literals. (3) Using deletion strategy, input half-lock resolution is complete for a Horn set.