Dieses Kapitel beschäftigt sich damit, wie die im vorigen Kapitel eingeführten semantischen Begriffe algorithmisch behandelt werden können. Diese Frage erfordert zunächst eine Präzisierung des Beweisbegriffs. Danach werden je eine Beweismethode für die Aussagenlogik und für die Prädikatenlogik erster Stufe eingeführt und ihre Eigenschaften untersucht.