Assertion Level Proof Planning with Compiled Strategies
Buch in deiner Nähe kaufen
Beschreibung
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.
Autor*in
Dominik Dietrich
Themen in »Assertion Level Proof Planning with Compiled Strategies«
CORE assertion level backward aplication declarative proof declarative tactic deduction modul deep aplication deep inference inference paradigm level proof proof planning proof planning proof refinement proof scripts proof strategies