LEADER 00000nam a22004453i 4500 
001    EBC267724 
003    MiAaPQ 
005    20200713055111.0 
006    m     o  d |       
007    cr cnu|||||||| 
008    200713s2006    xx      o     ||||0 eng d 
020    9781607501800|q(electronic bk.) 
020    |z9781586036256 
035    (MiAaPQ)EBC267724 
035    (Au-PeEL)EBL267724 
035    (CaPaEBR)ebr10152502 
035    (CaONFJC)MIL54767 
035    (OCoLC)71214605 
040    MiAaPQ|beng|erda|epn|cMiAaPQ|dMiAaPQ 
050  4 QA76.9.A96 -- N38 2006eb 
082 0  511.3 
100 1  Schwichtenberg, H 
245 10 Proof Technology and Computation 
264  1 Amsterdam :|bIOS Press,|c2006 
264  4 |c©2006 
300    1 online resource (456 pages) 
336    text|btxt|2rdacontent 
337    computer|bc|2rdamedia 
338    online resource|bcr|2rdacarrier 
505 0  Title page -- Preface -- Contents -- Information-Intensive
       Proof Technology -- Introduction to Proof Theory -- The 
       Abstraction-Refinement Framework in Model Checking -- 
       Verification: Industrial Applications -- Selected Topics 
       on Computability, Complexity, and Termination -- Jinja: 
       Towards a Comprehensive Formal Semantics for a Java-like 
       Language -- The Formulae-as-Classes Interpretation of 
       Constructive Set Theory -- Constructive Analysis with 
       Witnesses -- Predicates as Types -- Automata- and Logic-
       Based Systems Design -- Recursions and Proofs -- Author 
       Index 
520    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 
588    Description based on publisher supplied metadata and other
       sources 
590    Electronic reproduction. Ann Arbor, Michigan : ProQuest 
       Ebook Central, 2020. Available via World Wide Web. Access 
       may be limited to ProQuest Ebook Central affiliated 
       libraries 
650  0 Automatic theorem proving -- Congresses.;Computer 
       programming -- Congresses.;Computer software -- 
       Development -- Congresses 
655  4 Electronic books 
700 1  Spies, K 
700 1  NATO Advanced Study Institute on Proof Technology and 
       Computation, 
776 08 |iPrint version:|aSchwichtenberg, H.|tProof Technology and
       Computation|dAmsterdam : IOS Press,c2006|z9781586036256 
856 40 |uhttps://ebookcentral.proquest.com/lib/sinciatw/
       detail.action?docID=267724|zClick to View