Assertion Level Proof Planning with Compiled Strategies
- Brand: Dietrich, Dr. Dominik
- Availability: In stock
- SKU: 9783863760199
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...
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 sequential 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.
- Title: Assertion Level Proof Planning with Compiled Strategies
- Author: Dr. Dominik Dietrich
- Edition: 1st edition
- University: Saarland University
- Published: 1st edition 08/10/2012
- Department: electrical engineering and information technology
- Product Type: Book (Hardcover)
- Product type: Dissertation
- Language: English
- Binding: Softcover (paperback)
- Dimensions: 21.0 x 14.8 cm (DIN A5)
- Extent: XX / 341 pages
- Condition: New (shrink-wrapped in foil)
- Keywords: assertion level, backward application, CORE, declarative proof, declarative tactic, deduction modul, deep application, deep inference, inference paradigm, level proof, proof planning, proof refinement, proof scripts, proof strategies, proof theory, tautologies
Dominik Dietrich was born in 1980 in Saarbrücken, Germany. He studied Computer science and Mathematics at Saarland University in Saarbrücken, where he earned his Ph.D in 2011 under the supervision of Jörg Siekmann. His research focuses on automated reasoning, formal methods, and semantic based data and process management. Dominik is currently working as a researcher in the Cyber Physical Systems department of the German Research Center for Artificial Intelligence (DFKI) in Bremen.
DRM: Digital Watermark
This eBook contains a digital watermark and is therefore personalized for you. If the eBook is passed on to third parties abusively, it is possible to trace it back to the source.
File format: PDF (Portable Document Format)
With a fixed page layout, the PDF is particularly suitable for specialist books with columns, tables and figures. A PDF can be displayed on almost all devices, but is only suitable to a limited extent for small displays (smartphone, e-reader).
PC/Mac: You can read this eBook with a PC or Mac. You need a PDF viewer - e.g. Adobe Reader.
eReader: This eBook can be read with (almost) all eBook readers. However, it is not compatible with the Amazon Kindle.
Smartphone/Tablet: Whether Apple or Android, you can read this eBook. You need a PDF viewer - e.g. Adobe Reader.
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook orders from other countries.