Assertion level proof planning with compiled strategies
Dominik Dietrich · Publications of the UdS (Saarland University) · 2011
The objective of this thesis is to ease the formalization of proofs by being able to verify as well as to automatically construct abstract human-style proofs. This is achieved by lifting the logical basis to the abstract assertion level, which has been identified as a style of reasoning that can be found in textbooks. A case study shows that automatic reasoning procedures benefit from the abstract assertion level reasoning. In addition, a strategy language is developed that allows the specification of abstract underspecified declarative proof patterns within the proof document and supports their refinement. Case studies show that complex reasoning patterns can concisely be specified within the developed language. Together, the complementary methods provide a framework to automate declarative proofs at the assertion level.