Advances in equational theorem proving [Elektronische Ressource] : architecture, algorithms, and redundancy avoidance / von Bernd Löchner

Advances inEquational Theorem Proving{Architecture, Algorithms, andRedundancy AvoidanceVom Fachbereich Informatikder Technischen Universit˜ at Kaiserslauternzur Verleihung des akademischen GradesDoktor der Naturwissenschaften (Dr. rer. nat.)genehmigte DissertationvonDipl.-Inform. Bernd L˜ ochnerDatum der wissenschaftlichen Aussprache: 20. Juli 2005Dekan: Prof. Dr. Reinhard GotzheinPrufungsk˜ ommision:Vorsitzender: Prof. Dr. Arnd Poetzsch-HefiterBerichterstatter: Prof. Dr. Jurgen˜ AvenhausProf. Dr. Klaus E. MadlenerD 386Beflehl Du Deine Wege und was Dein Herze kr˜ ankt,der allertreusten P ege des, der den Himmel lenkt.Der Wolken, Luft und Winden gibt Wege, Lauf und Bahn,der wird auch Wege flnden, da Dein Fu… gehen kann.Ihn, ihn la… tun und walten, er ist ein weiser Furst˜und wird sich so verhalten, da… Du Dich wundern wirst,wenn er, wie ihm gebuhret,˜ mit wunderbarem Ratdas Werk hinausgefuhret,˜ das Dich bekummert˜ hat.Paul GerhardZusammenfassungAutomatisches Theorembeweisen ist ein spezielles Suchproblem, das aufgrund seinerUnentscheidbarkeit sehr schwierig ist. Die Herausforderung bei der Entwicklung prak-tisch leistungsf˜ ahiger Beweiser liegt darin, die reich entwickelte Theorie so in ein Pro-gramm abzubilden, da… dieses e–zient auf dem Rechner l˜auft.