Resolution

<=> Prädikatenlogik

==> Klausel

==> Horn-Klausel

<=> Inferenzregel

==> Beweisen, automatisches

<== Theorembeweiser

==> Logikprogrammierung

<=> Prolog

<== Künstliche Intelligenz, Geschichte der

<== Deduktion

==> Subsumtion, Subsumption

==> Unifikation