Klausel

==> Prädikatenlogik

<== Horn-Klausel

<== Resolution

==> Skolemisierung

==> Quantor

==> Formel

==> Disjunktion

==> Implikation

==> Konjunktion