Abstract. For two fragments LP and LF of monadic first-order logic with bounded quantifiers, the corresponding versions of specification theorem are formulated and proved, which enables the ∑-automata synthesis procedure to be reduced to the equivalent transformation of formulas.

Keywords: first order logics, specification, ∑-automaton, LP-formula, LF-formula, automatic semantics, specification theorem .