Hierarchical contextual reasoning [Elektronische Ressource] / Serge Autexier

Hierarchical Contextual ReasoningSerge AutexierDissertation zur Erlangung des GradesDoktor der Ingenieurwissenschaften (Dr.-Ing.)der Naturwissenschaftlich-Technischen Fakultat¤ Ider Universitat¤ des SaarlandesSaarbruck¤ en, 2003Dekan Prof. Dr. Philipp SlusallekVorsitzender Prof. Dr. Reinhard WilhelmGutachter Prof. Dr. (PhD) Jor¤ g Siekmann, Universitat¤ des SaarlandesProf. Dr. (PhD) Frank Pfenning, Carnegie Mellon University, Pittsburgh, USAProf. Dr. Gert Smolka, Universitat¤ des SaarlandesKolloquium 19. Dezember 2003ContentsKurzzusammenfassung VAbstract VIIZusammenfassung IXExtended Abstract XIAcknowledgements XIIII Introduction 11 Introduction 31.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.1.1 Communication of Proof Knowledge . . . . . . . . . . . . . . . . . . . . . 31.1.2 Proof Construction Steps and Proof History . . . . . . . . . . . . . . . . . . 41.1.3 Status of Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.2 The CORE System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.3 Overview of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 Historical Overview and State of the Art 112.1 Foundations of Mechanised Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . 122.2 Development of Programs for Mechanised Reasoning . . . . . . . . . . . . . . . . . 132.3 Application of for . . . . . . . . . . . . .