Proof technology and computation /

Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient. The chapters deal with: The benefits and technical challenges of sharing formal mathematics among interactive theorem provers; proof normalization for vari...

وصف كامل

التفاصيل البيبلوغرافية
مؤلف مشترك: NATO Advanced Study Institute on Proof Technology and Computation Marktoberdorf, Germany
مؤلفون آخرون: Schwichtenberg, Helmut, 1942-, Spies, Katharina
التنسيق: Licensed eBooks
اللغة:الإنجليزية
منشور في: Amsterdam ; Washington, DC : IOS Press, ©2006.
سلاسل:NATO science series. Computer and systems sciences ; v. 200.
الوصول للمادة أونلاين:https://search.ebscohost.com/login.aspx?direct=true&scope=site&db=nlebk&AN=165586
الوصف
الملخص:Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient. The chapters deal with: The benefits and technical challenges of sharing formal mathematics among interactive theorem provers; proof normalization for various axiomatic theories; abstraction-refinement framework of temporal logic model checking; formal verification in industrial hardware design; readable machine-checked proofs and semantics and more.
وصف المادة:"Proceedings of the NATO Advanced Study Institute on Proof Technology and Computation, Marktoberdorf, Germany, 29 July-10 August 2003"--Title page verso.
"Published in cooperation with NATO Public Diplomacy Division."
وصف مادي:1 online resource
بيبلوغرافيا:Includes bibliographical references and index.
ردمك:1423797558
9781423797555
1601294840
9781601294845
9781607501800
1607501805
661054767X
1280547677
9781280547676
9786610547678
6000005288
9786000005283
1586036254
9781586036256
تدمد:1387-6694 ;