Es wird gezeigt, daß Shannon-Graphen eine für das automatische Beweisen geeignete Darstellung von logischen Formeln sind. Der Shannon-Graph einer aussagenlogischen Formel F enthält sowohl Information über die Modelle von F als auch über die Modelle von not F. Dies hat zur Folge, daß die Beweisverfahren für Shannon-Graphen die aus dem Tableaukalkül bekannte Lemma-Generierung ``automatisch'' beinhalten. Die vorgestellten Verfahren können durch Verwendung einer bestimmten übersetzungstechnik effizient implementiert werden. Die Grundidee dieser übersetzung besteht darin, aus der Darstellung einer Formel F in Form eines Shannon-Graphen ein Programm zu generieren, das die Suche nach einer Widerlegung speziell für F vornimmt.
In dieser Arbeit werden die theoretischen Grundlagen von Shannon-Graphen und den darauf aufbauenden Beweisverfahren behandelt und gezeigt, daß diese Verfahren korrekt und vollständig sind. Auf die Realisierung der Verfahren wird ausführlich eingegangen und die Implementierung des im Rahmen dieser Arbeit entstandenen Beweisers beschrieben.