Assertion level proof planning with compiled strategies

This book presents new techniques that allow the automatic verification and generation of abstract human-style proofs. The core of this approach builds an efficient calculus that works directly by applying definitions, theorems, and axioms, which reduces the size of the underlying proof object by a factor of ten. The calculus is extended by the deep inference paradigm which allows the application of inference rules at arbitrary depth inside logical expressions and provides new proofs that are exponentially shorter and not available in the sequent calculus without cut. In addition, a strategy language for abstract underspecified declarative proof patterns is developed. Together, the complementary methods provide a framework to automate declarative proofs. The benefits of the techniques are illustrated by practical applications.