Sortenlogik

==> Beweisen, automatisches

==> Prädikatenlogik

<== Inferenzverfahren

==> Unifikation

<== Parsing natürlicher Sprache