Аннотация. Для двух фрагментов, LP и LF, логики первого порядка с ограниченными кванторами сформулированы и доказаны соответствующие варианты теоремы о спецификации, позволяющие свести процедуру синтеза ∑-автоматов, специфицированных формулами этих логик, к эквивалентному преобразованию формул.

Ключевые слова: логики первого порядка, спецификация, ∑-автомат, LP-формула, LF-формула, автоматная семантика, теорема о спецификации.