Skolemisierung

==> Prädikatenlogik

<== Klausel

<== Modelltheorie

==> Beweisen, automatisches

==> Äquivalenz