Use of unit clauses and clause splitting in automatic deduction

A mechanical theorem prover usually has to perform unification which is a very time-consuming operation. Therefore, it is necessary to reduce the number of unification operations to obtain speedups. There are two ways to do this. One is to restrict the literals to be unified with the underlying literal, and the other is to make clauses small. Four techniques: unit simplification, ground unit clause generation, UR simulation, and small proof checking, can restrict the literals to be unified with. All these techniques take advantage of unit clauses. The clause splitting technique is able to reduce the length of a clause by splitting the clause into shorter clauses. These techniques improve dramatically the efficiency of a theorem prover, using the hyper-linking method, in many cases.>