LEADER 03848nam 22007935 450 001 996466054603316 005 20240619233401.0 010 $a3-642-22863-1 024 7 $a10.1007/978-3-642-22863-6 035 $a(CKB)2550000000052364 035 $a(SSID)ssj0000610044 035 $a(PQKBManifestationID)11373584 035 $a(PQKBTitleCode)TC0000610044 035 $a(PQKBWorkID)10639499 035 $a(PQKB)11598923 035 $a(DE-He213)978-3-642-22863-6 035 $a(MiAaPQ)EBC3067158 035 $a(PPN)156313170 035 $a(EXLCZ)992550000000052364 100 $a20110808d2011 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aInteractive Theorem Proving $eSecond International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings /$fedited by Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk 205 $a1st ed. 2011. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2011. 215 $a1 online resource (XI, 383 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6898 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-22862-3 320 $aIncludes bibliographical references and index. 327 $aTowards verification of product lines (abstract) / Don Batory -- Advances in the formalization of the odd order theorem / Georges Gonthier -- Logical formalisation and analysis of the Mifare classic card in PVS / Bart Jacobs, Ronny Wichers Schreur. 330 $aThis book constitutes the refereed proceedings of the Second International Conference on Interactive Theorem proving, ITP 2011, held in Berg en Dal, The Netherlands, in August 2011. The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6898 606 $aComputer science 606 $aSoftware engineering 606 $aMachine theory 606 $aCompilers (Computer programs) 606 $aArtificial intelligence 606 $aComputer programming 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aFormal Languages and Automata Theory 606 $aCompilers and Interpreters 606 $aArtificial Intelligence 606 $aProgramming Techniques 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aMachine theory. 615 0$aCompilers (Computer programs). 615 0$aArtificial intelligence. 615 0$aComputer programming. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aFormal Languages and Automata Theory. 615 24$aCompilers and Interpreters. 615 24$aArtificial Intelligence. 615 24$aProgramming Techniques. 676 $a005.1015113 702 $aEekelen$b M. C. J. D. van$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aGeuvers$b Herman$f1964-.$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSchmaltz$b Julien$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aWiedijk$b Freek$f1961-.$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996466054603316 996 $aInteractive Theorem Proving$92010767 997 $aUNISA LEADER 01123nam2 22002893i 450 001 BRI0009708 005 20251003044047.0 010 $a8802034575 100 $a20050530d1980 ||||0itac50 ba 101 | $aita 102 $ait 181 1$6z01$ai $bxxxe 182 1$6z01$an 200 0 $a2$fGalileo Galilei 205 $a2. ed. riveduta e corretta 210 $aTorino$cUnione Tipografico-Editrice Torinese$d1980 215 $a851 p., [6] carte di tav.$cill.$d24 cm. 461 1$1001NAP0323965$12001 $aOpere di Galileo Galilei$fa cura di Franz Brunetti$v2 676 $a500$9SCIENZE NATURALI E MATEMATICA$v21 676 $a501$9SCIENZE NATURALI E MATEMATICA. FILOSOFIA E TEORIA$v21 801 3$aIT$bIT-000000$c20050530 850 $aIT-BN0095 $aIT-AV0007 $aIT-NA0079 $aIT-AV0045 912 $aBRI0009708 950 2$aBiblioteca Centralizzata di Ateneo$c14 v. (Alcuni in pił tomi)$d 01COLL. ITA CLADSC$e 01AR 0070032505 VMA (0008.2 v. 2$fB $h20250512$i20250512 977 $a 01$a AV$a BN$a MV 996 $a2$961340 997 $aUNISANNIO