Automatische Theorembeweiser sind Computerprogramme, die mit mathematischer Genauigkeit beweisen, dass eine Vermutung zwingend aus einer Menge von Axiomen folgt. Axiome und Vermutung sind dabei Formeln z. B. der Prädikatenlogik erster Stufe. Die Formeln werden logisch kombiniert, um daraus neue Fakten abzuleiten. Die Anzahl der möglichen Ableitungen ist enorm groß, und nur wenige führen zum Ziel. Theorembeweiser müssen möglichst schnell kombinieren, aber ebenso entscheiden, welche der vielen möglichen Ableitungen sie verfolgen. Damit sind sie sowohl ein Werkzeug als auch ein Gegenstand der Künstlichen Intelligenz.

Die CADE veranstaltet seit 1996 jährlich die CADE ATP System Competition, um die Leistungen von Beweisern zu vergleichen. Dabei versuchen die Systeme in verschiedenen Kategorien möglichst viele Aufgaben zu lösen.

Der an der DHBW Stuttgart entwickelte Beweiser E gewann in der Kategorie UEQ den ersten Platz. In der Königsklasse (Formeln der Prädikatenlogik erster Stufe) erreichte E nach dem Beweiser Vampire der University of Manchester den zweiten Platz. Ebenfalls für den zweiten Platz reichte es in der Kategorie LTB. Neben den direkten Erfolgen war E auch indirekt an den Systemen Satallax und LEO-III, den Siegern zweier Kategorien beteiligt, indem diese E verwendeten, um Teilprobleme zu lösen.