Der vorliegende Band, der sich insbesondere an Studienanfänger/innen der Informatik und benachbarter Disziplinen richtet, gibt eine Einführung in die grundlegenden Techniken und Methoden der formalen Logik und in die Möglichkeiten der Logikprogrammierung am Beispiel der Programmiersprache Prolog. Der Schwerpunkt liegt neben der Darstellung von Syntax und Semantik der Aussagen- und der Prädikatenlogik auf der Entwicklung von automatisierten Beweisverfahren (Resolutions- und Tableauverfahren, Konnektionsmethode, Hilbert-Systeme 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 Spezifizierung und Prüfung von Algorithmen zu ermöglichen. Im Schlußteil des Bandes wird dann der Übergang vom automatischen Beweisen zum Programmieren in Prolog vollzogen und eine formale Semantik für die deklarativen Anteile von Prolog vorgestellt. Der Band enthält zahlreiche Übungsaufgaben, die die vertiefte Einarbeitung in die dargestellten Methoden ermöglichen.