Handbook of Automated Reasoning

5 Global Design Decisions

5.1 Main-Loop

The main-loop without splitting, Table 4, is a generalization of the main-loop introduced in Section 3, Table 1.

Table 4

The Overall Loop without Splitting

1	Prover(N)
2	$Wo:=\varnothing$ ;
3	Us := ired(N,N);
4	While $\left(Us\ne \varnothing \text{and}\square \notin Us\right)\{$
5	(Given, Us)   := choose(Us);
6	Wo     := Wo ∪ {Given};
7	New     := inf (Given, Wo);
8	(New, Wo, Us)  := ired(New, Wo, Us);
9	}
10	If $\left(Us=\varnothing \right)$ then print “Completion Found”;
11	If ( ∈