Prädikatenlogische Fragestellungen wie die nach der Allgemeingültigkeit oder der Erfüllbarkeit einer Formel sind zwar im Allgemeinen nicht entscheidbar, für konkrete Fälle gibt es aber Methoden, die häufig eine Antwort liefern. Dieses Kapitel stellt praktikable Herangehensweisen an solche Fragestellungen vor: die Tableau-Methode und den Satz von Herbrand einschließlich Unifikation und Resolution.