DHBW-Horn-clauses-resolver Variablen n–z (+Integer) Funktionen a–m (+Integer) Prädikate A–Z (+Integer) Junktoren &, -> Bool-Konstanten true, false Klammern (, )