New proof of the solvability of the elementary theory of linearly ordered sets (Q923067)

The first-order theory of linearly ordered sets (LOS) is known to be decidable. Two proofs of its decidability were proposed. \textit{H. Läuchli} and \textit{J. Leonard} [Fundam. Math. 59, 109-116 (1966; Zbl 0156.253)] proved it by presenting a constructive description of countermodels; this proof gives no explicit upper time-bound. Rabin's proof [\textit{M. O. Rabin}, Handbook of Mathematical Logic, Stud. Logic Found. Math. 90, 595-629 (1977; Zbl 0443.03001)] is by embedding LOS to the theory S2S of two successor functions; it gives an upper time-bound of the algorithm, and also a lower bound. The author gives a straightforward decidability algorithm with the same upper bound as Rabin's. The idea is to associate a finite set of ``feasible projects'' to each theory T; a project is a sequence \(T_ 0,a_ 1,T_ 1,...,a_ k,T_ k\) of theories and constants. Then, by constructing paths in the set of all feasible projects, we either obtain a model for T or prove that T is inconsistent.