Les automates cellulaires sont un modèle de calcul parallèle et local. Ce poster présente une caractérisation en logique de Horn du temps minimal des automates cellulaires en une dimension, le comportement local et déterministe des automates cellulaires s'exprimant naturellement par des clauses de Horn portant sur une arithmétique locale du successeur.
L'outil principal utilisé est une méthode de normalisation transformant une formule en une formule équivalente qui imite un circuit grille.