Der vorliegende Band, der sich insbesondere an Studierende der Informatik und benachbarter Disziplinen richtet, gibt eine Einführung in die grundlegenden Techniken und Methoden der formalen Logik und die Möglichkeiten der Logikprogrammierung am Beispiel der Programmiersprache Prolog. Der Schwerpunkt liegt neben der Darstellung von Syntax und Semantik der Aussagen- und Prädikatenlogik auf der Entwicklung von automatisierten Beweisverfahren (Resolutions- und Tableauverfahren, Konnektionsmethode u.a.) sowie dem sog. Kalkül des natürlichen Schließens, der zahlreiche auch in der Mathematik verwendete Beweistechniken vermittelt. Die Logik-Programmiersprache Prolog wird zunächst informell eingeführt, um in diesem Rahmen die Spezifikation und das Austesten von Algorithmen zu ermöglichen. Im Schlussteil des Bandes wird dann der Übergang vom automatisierten Beweisen zum Programmieren in Prolog vollzogen und eine formale Semantik für die deklarativen Teile von Prolog vorgestellt. Der Band stellt die überarbeitete und erweiterte Fassung der bewährten einbändigen Ausgabe des Werks dar, der durch einen umfangreichen Übungsband ergänzt wird.