LEADER 05256nam 22007335 450 001 996466102203316 005 20200629194036.0 010 $a3-540-49801-X 024 7 $a10.1007/BFb0055125 035 $a(CKB)1000000000210979 035 $a(SSID)ssj0000327169 035 $a(PQKBManifestationID)11213082 035 $a(PQKBTitleCode)TC0000327169 035 $a(PQKBWorkID)10316432 035 $a(PQKB)11531550 035 $a(DE-He213)978-3-540-49801-8 035 $a(PPN)155178792 035 $a(EXLCZ)991000000000210979 100 $a20121227d1998 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTheorem Proving in Higher Order Logics$b[electronic resource] $e11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings /$fedited by Jim Grundy, Malcolm Newey 205 $a1st ed. 1998. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1998. 215 $a1 online resource (IX, 496 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1479 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-64987-5 327 $aVerified lexical analysis -- Extending window inference -- Program abstraction in a higher-order logic framework -- The village telephone system: A case study in formal software engineering -- Generating embeddings from denotational descriptions -- An interface between CLAM and HOL -- Classical propositional decidability via Nuprl proof extraction -- A comparison of PVS and Isabelle/HOL -- Adding external decision procedures to HOL90 securely -- Formalizing basic first order model theory -- Formalizing Dijkstra -- Mechanical verification of total correctness through diversion verification conditions -- A type annotation scheme for Nuprl -- Verifying a garbage collection algorithm -- Hot: A concurrent automated theorem prover based on higher-order tableaux -- Free variables and subexpressions in higher-order meta logic -- An LPO-based termination ordering for higher-order terms without ?-abstraction -- Proving isomorphism of first-order logic proof systems in HOL -- Exploiting parallelism in interactive theorem provers -- I/O automata and beyond: Temporal logic and abstraction in Isabelle -- Object-oriented verification based on record subtyping in Higher-Order Logic -- On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system -- Co-inductive axiomatization of a synchronous language -- Formal specification and theorem proving breakthroughs in geometric modeling -- A tool for data refinement -- Mechanizing relevant logics with HOL -- Case studies in meta-level theorem proving -- Formalization of graph search algorithms and its applications. 330 $aThis book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '98, held in Canberra, Australia, in September/October 1998. The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1479 606 $aComputer logic 606 $aArtificial intelligence 606 $aSoftware engineering 606 $aMathematical logic 606 $aLogic design 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 615 0$aComputer logic. 615 0$aArtificial intelligence. 615 0$aSoftware engineering. 615 0$aMathematical logic. 615 0$aLogic design. 615 14$aLogics and Meanings of Programs. 615 24$aArtificial Intelligence. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aMathematical Logic and Formal Languages. 615 24$aSoftware Engineering. 615 24$aLogic Design. 676 $a004/.01/5113 702 $aGrundy$b Jim$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aNewey$b Malcolm$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTPHOLs '98 906 $aBOOK 912 $a996466102203316 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNISA LEADER 01287nam 2200349Ia 450 001 996395959903316 005 20200824132751.0 035 $a(CKB)4940000000056335 035 $a(EEBO)2240951843 035 $a(OCoLC)ocm12114218e 035 $a(OCoLC)12114218 035 $a(EXLCZ)994940000000056335 100 $a19850604d1643 uy | 101 0 $aeng 135 $aurbn||||a|bb| 200 13$aAn ordinance of the Lords and Commons assembled in Parliament$b[electronic resource] $econcerning all brewers and makers of beere, ale, cider, or perry, for payment of the excise imposed by an ordinance of Parliament, before the delivering thereof, upon paine of forfeiture of double the value of the said commodities 210 $aLondon $cPrinted by Richard Cotes and John Raworth$d1643 215 $a[2], 23-28 p 300 $aReel 240:E75, no. 15. 300 $aReproduction of original in Thomason Collection, British Library. 330 $aeebo-0158 606 $aInternal revenue$zEngland 615 0$aInternal revenue 801 0$bEAA 801 1$bEAA 801 2$bm/c 801 2$bUMI 801 2$bWaOLN 906 $aBOOK 912 $a996395959903316 996 $aAn ordinance of the Lords and Commons assembled in Parliament$92298865 997 $aUNISA LEADER 01944nam a2200313 i 4500 001 991002619519707536 008 141027s2014 it a 000 0 ita d 020 $a9788896764527 035 $ab14204046-39ule_inst 040 $aBibl. Dip.le Aggr. Ingegneria Innovazione - Sez. Ingegneria Innovazione$beng 082 0 $a531.09 245 00$aStoria della Meccanica /$ca cura di Virgilio Cantoni, Vittorio Marchis, Edoardo Rovida 260 $aPavia :$bPavia University Press,$cc2014 300 $a2 v. :$bill. ;$c24 cm 650 4$aMechanics$xHistory 700 1 $aCantoni, Virginio 700 1 $aMarchis, Vittorio 700 1 $aRovida, Edoardo 907 $a.b14204046$b14-09-21$c30-10-14 912 $a991002619519707536 945 $aLE026 531.09 D CAN 01.01 V.I C.1 2014 $cV.1 - C.1$g1$i2026000068954$lle026$nProf. Dattoma / Biblioteca$op$pE29.50$q-$rn$s- $t1$u0$v0$w0$x0$y.i1564599x$z26-11-14 945 $aLE026 531.09 D CAN 01.01 V.I C.2 2014 $cV.1 - C.2$g1$i2026000068961$lle026$nProf. Dattoma / Biblioteca$op$pE29.50$q-$rl$s- $t0$u0$v0$w0$x0$y.i15646002$z26-11-14 945 $aLE026 531.09 D CAN 01.01 V.I C.3 2014 $cV.1 - C.3$g1$i2026000068978$lle026$nProf. Dattoma / Biblioteca$op$pE29.50$q-$rl$s- $t0$u0$v0$w0$x0$y.i15646014$z26-11-14 945 $aLE026 531.09 D CAN 01.01 V.II C.1 2014 $cV.2 - C.1$g1$i2026000068985$lle026$nProf. Dattoma / Biblioteca$op$pE29.50$q-$rn$s- $t1$u0$v0$w0$x0$y.i15646026$z26-11-14 945 $aLE026 531.09 D CAN 01.01 V.II C.2 2014 $cV.2 - C.2$g1$i2026000068992$lle026$nProf. Dattoma / Biblioteca$op$pE29.50$q-$rl$s- $t0$u0$v0$w0$x0$y.i15646038$z26-11-14 945 $aLE026 531.09 D CAN 01.01 V.II C.3 2014 $cV.2 - C.3$g1$i2026000069005$lle026$nProf. Dattoma / Biblioteca$op$pE29.50$q-$rl$s- $t0$u0$v0$w0$x0$y.i15646051$z26-11-14 996 $aStoria della Meccanica$9258278 997 $aUNISALENTO 998 $ale026$b27-10-14$cm$da $e-$fita$git $h0$i0