Eine Rechnung von A mit Eingabeterm t ist eine Folge von Regelanwendungen.
Beispiel: Eingabe t = F (T F), Rechnung F (T F)0 (T F)0 (1 F)0 (1 0)0 0 0.
Eine akzeptierende Rechnung endet mit einem q F. Wir schreiben tq F.
Die Sprache des Automaten ist L(A) = {t | q F : tq}.
Die Sprache des Beispiel-Automaten sind genau die Formeln mit Wahrheitswert 1.
Übung: warum gibt es in Baum-Automaten keine Startzustände?
Übung: geben Sie einen Baumautomaten für die Menge aller allgemeingültigen aussagenlogischen Formeln über dem Alphabet {x, T, F,¬, , } mit einer Variablen x an (Beispiel: x ¬x gehört dazu.) Hinweis: der Automat hat 4 Zustände.