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

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