|
|
|
|
| LEADER |
00000cam a2200000 a 4500 |
| 001 |
ocm71214605 |
| 003 |
OCoLC |
| 005 |
20240809213013.0 |
| 006 |
m o d |
| 007 |
cr cnu---unuuu |
| 008 |
060830s2006 ne ob 101 0 eng d |
| 040 |
|
|
|a N$T
|b eng
|e pn
|c N$T
|d OCLCG
|d OCLCQ
|d TUU
|d OCLCQ
|d OCLCF
|d OCLCO
|d OCLCQ
|d CCO
|d E7B
|d YDXCP
|d UV0
|d DKDLA
|d IOSPR
|d IDEBK
|d MHW
|d DEBSZ
|d OCLCO
|d EBLCP
|d OCL
|d OCLCQ
|d OCLCO
|d OCL
|d OCLCO
|d AZK
|d CNNLC
|d AGLDB
|d MOR
|d PIFBR
|d ZCU
|d MERUC
|d OCLCQ
|d WY@
|d U3W
|d LUE
|d STF
|d BRL
|d WRM
|d JBG
|d OCLCQ
|d VTS
|d NRAMU
|d EZ9
|d ICG
|d INT
|d VT2
|d OCLCQ
|d WYU
|d G3B
|d TKN
|d OCLCQ
|d DKC
|d AU@
|d OCLCQ
|d M8D
|d OCLCQ
|d OCL
|d OCLCQ
|d K6U
|d OCL
|d OCLCO
|d OCLCQ
|d QGK
|d OCLCO
|d OCLCL
|d OCLCQ
|d OCLCL
|d OCLCQ
|
| 019 |
|
|
|a 191037987
|a 228146679
|a 228146680
|a 467112992
|a 473863657
|a 491260157
|a 567966437
|a 647632847
|a 888710007
|a 961548797
|a 962677909
|a 1037508696
|a 1259277765
|
| 020 |
|
|
|a 1423797558
|q (electronic bk.)
|
| 020 |
|
|
|a 9781423797555
|q (electronic bk.)
|
| 020 |
|
|
|a 1601294840
|
| 020 |
|
|
|a 9781601294845
|
| 020 |
|
|
|a 9781607501800
|
| 020 |
|
|
|a 1607501805
|
| 020 |
|
|
|z 1586036254
|
| 020 |
|
|
|z 9781586036256
|
| 020 |
|
|
|a 661054767X
|
| 020 |
|
|
|a 1280547677
|
| 020 |
|
|
|a 9781280547676
|
| 020 |
|
|
|a 9786610547678
|
| 020 |
|
|
|a 6000005288
|
| 020 |
|
|
|a 9786000005283
|
| 024 |
3 |
|
|z 9781586036256
|
| 035 |
|
|
|a (OCoLC)71214605
|z (OCoLC)191037987
|z (OCoLC)228146679
|z (OCoLC)228146680
|z (OCoLC)467112992
|z (OCoLC)473863657
|z (OCoLC)491260157
|z (OCoLC)567966437
|z (OCoLC)647632847
|z (OCoLC)888710007
|z (OCoLC)961548797
|z (OCoLC)962677909
|z (OCoLC)1037508696
|z (OCoLC)1259277765
|
| 037 |
|
|
|a 978-1-58603-625-6
|b IOS Press
|n http://www.iospress.nl
|
| 050 |
|
4 |
|a QA76.9.A96
|b N38 2003eb
|
| 072 |
|
7 |
|a COM
|x 025000
|2 bisacsh
|
| 049 |
|
|
|a HCDD
|
| 111 |
2 |
|
|a NATO Advanced Study Institute on Proof Technology and Computation
|d (2003 :
|c Marktoberdorf, Germany)
|
| 245 |
1 |
0 |
|a Proof technology and computation /
|c edited by Helmut Schwichtenberg and Katharina Spies.
|
| 260 |
|
|
|a Amsterdam ;
|a Washington, DC :
|b IOS Press,
|c ©2006.
|
| 300 |
|
|
|a 1 online resource
|
| 336 |
|
|
|a text
|b txt
|2 rdacontent
|
| 337 |
|
|
|a computer
|b c
|2 rdamedia
|
| 338 |
|
|
|a online resource
|b cr
|2 rdacarrier
|
| 347 |
|
|
|a data file
|2 rda
|
| 490 |
1 |
|
|a NATO science series. Series III, Computer and systems sciences,
|x 1387-6694 ;
|v v. 200
|
| 500 |
|
|
|a "Proceedings of the NATO Advanced Study Institute on Proof Technology and Computation, Marktoberdorf, Germany, 29 July-10 August 2003"--Title page verso.
|
| 500 |
|
|
|a "Published in cooperation with NATO Public Diplomacy Division."
|
| 504 |
|
|
|a Includes bibliographical references and index.
|
| 505 |
0 |
|
|a 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 |
|
|
|a 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.
|
| 546 |
|
|
|a English.
|
| 650 |
|
0 |
|a Automatic theorem proving
|v Congresses.
|
| 650 |
|
0 |
|a Computer programming
|v Congresses.
|
| 650 |
|
0 |
|a Computer software
|x Development
|v Congresses.
|
| 650 |
|
7 |
|a COMPUTERS
|x Expert Systems.
|2 bisacsh
|
| 650 |
|
7 |
|a Automatic theorem proving
|2 fast
|
| 650 |
|
7 |
|a Computer programming
|2 fast
|
| 650 |
|
7 |
|a Computer software
|x Development
|2 fast
|
| 655 |
|
7 |
|a Conference papers and proceedings
|2 fast
|
| 700 |
1 |
|
|a Schwichtenberg, Helmut,
|d 1942-
|1 https://id.oclc.org/worldcat/entity/E39PBJjdhThBtcGRtbyq7d6Myd
|
| 700 |
1 |
|
|a Spies, Katharina.
|
| 776 |
0 |
8 |
|i Print version:
|a NATO Advanced Study Institute on Proof Technology and Computation (2003 : Marktoberdorf, Germany).
|t Proof technology and computation.
|d Amsterdam ; Washington, DC : IOS Press, ©2006
|z 1586036254
|z 9781586036256
|w (DLC) 2006927922
|w (OCoLC)77528062
|
| 830 |
|
0 |
|a NATO science series.
|n Series III,
|p Computer and systems sciences ;
|v v. 200.
|x 1387-6694
|
| 856 |
4 |
0 |
|u https://ebookcentral.proquest.com/lib/holycrosscollege-ebooks/detail.action?docID=267724
|y Click for online access
|
| 903 |
|
|
|a EBC-AC
|
| 994 |
|
|
|a 92
|b HCD
|