一句话：用存在二阶 Horn 逻辑刻画一维元胞自动机实时（最小时间）复杂类，并给出网格电路归一化方法。
本文研究一维元胞自动机在最小时间（real-time）计算下的描述复杂度，旨在为并行计算模型提供自然的声明式程序设计方式。作者针对元胞自动机的三种经典规范变体，建立相应的逻辑刻画：所用逻辑是存在二阶 Horn 逻辑的自然限制，分别对应在边长 n 的方形网格电路上按输入词的三种规范摆放方式判定语言。关键工具是一种归一化方法，可将公式转化为忠实模拟网格电路的等价公式。由此得到实时元胞自动机复杂类与受限逻辑之间的精确对应。
Descriptive complexity may be useful to design programs in a natural declarative way. This is important for parallel computation models such as cellular automata, because designing parallel programs is considered difficult. Our paper establishes logical characterizations of the three classical complexity classes that model minimal time, called real-time, of one-dimensional cellular automata according to their canonical variants. Our logics are natural restrictions of the existential second-order Horn logic. They correspond to the three ways of deciding a language on a square grid circuit of side n according to the three canonical placements of an input word of length n on the grid. Our key tool is a normalization method that transforms a formula into an equivalent formula that faithfully mimics a grid circuit.