Аннотация:В работе рассматривается расширение темпоральной логики до логики первого порядка с одноместными предикатными символами, термы которой задаются арифметическими выражениями, составленными из операции сложения и констант. Такие термы, с одной стороны, позволяют устанавливать более глубокие связи между моментами времени, с другой – гарантируют разрешимость рассматриваемой логики. Для введенной логики автор построил алгоритм проверки истинности формул и доказал теорему о корректности и сходимости алгоритма.