TY  - THES
T1  - Assertion level proof planning with compiled strategies
T3  - Zugl. im Buchhandel: Göttingen : Optimus-Verl., 2012
A1  - Dietrich,Dominik
Y1  - 2012/08/25
N2  - 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.
KW  - Automatisches Beweisverfahren
KW  - Deduktion
KW  - Heuristik
KW  - deklarative Beweisstrategien 
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
SN  - 978-3-86376-019-9
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2012/4932
ER  -