LEADER 04853nam 22006255 450 001 996466143903316 005 20200702093931.0 010 $a3-540-48803-0 024 7 $a10.1007/3-540-58450-1 035 $a(CKB)1000000000234180 035 $a(SSID)ssj0000323781 035 $a(PQKBManifestationID)11258082 035 $a(PQKBTitleCode)TC0000323781 035 $a(PQKBWorkID)10300222 035 $a(PQKB)10167578 035 $a(DE-He213)978-3-540-48803-3 035 $a(PPN)155188003 035 $a(EXLCZ)991000000000234180 100 $a20121227d1994 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aHigher Order Logic Theorem Proving and Its Applications$b[electronic resource] $e7th International Workshop, Valletta, Malta, September 19-22, 1994. Proceedings /$fedited by Thomas F. Melham, Juanito Camilleri 205 $a1st ed. 1994. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1994. 215 $a1 online resource (XI, 477 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v859 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-58450-1 327 $aLCF examples in HOL -- A graphical tool for proving UNITY progress -- Reasoning about a class of linear systems of equations in HOL -- Towards a HOL theory of memory -- Providing tractable security analyses in HOL -- Highlighting the lambda-free fragment of Automath -- First-order automation for higher-order-logic theorem proving -- Symbolic animation as a proof tool -- Datatypes in L2 -- A formal theory of undirected graphs in higher-order logc -- Mechanical verification of distributed algorithms in higher-order logic -- Tracking design changes with formal verification -- Weak systems of set theory related to HOL -- Interval-semantic component models and the efficient verification of transaction-level circuit behavior -- An interpretation of Noden in HOL -- Reasoning about real circuits -- Binary decision diagrams as a HOL derived rule -- Trustworthy tools for trustworthy programs: A verified verification condition generator -- S: A machine readable specification notation based on higher order logic -- An engineering approach to formal digital system design -- Generating designs using an Algorithmic Register Transfer Language with formal semantics -- A HOL formalisation of the Temporal Logic of Actions -- Studying the ML module system in HOL -- Towards a mechanically supported and compositional calculus to design distributed algorithms -- Simplifying deep embedding: A formalised code generator -- Automating verification by functional abstraction at the system level -- A parameterized proof manager -- Implementational issues for verifying RISC-pipeline conflicts in HOL -- Specifying instruction-set architectures in HOL: A primer -- Representing higher-order logic proofs in HOL. 330 $aThis volume presents the proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications held in Valetta, Malta in September 1994. Besides 3 invited papers, the proceedings contains 27 refereed papers selected from 42 submissions. In total the book presents many new results by leading researchers working on the design and applications of theorem provers for higher order logic. In particular, this book gives a thorough state-of-the-art report on applications of the HOL system, one of the most widely used theorem provers for higher order logic. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v859 606 $aComputers 606 $aMathematical logic 606 $aArtificial intelligence 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aComputers. 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 14$aTheory of Computation. 615 24$aMathematical Logic and Foundations. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 676 $a004/.01/5113 702 $aMelham$b Thomas F$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aCamilleri$b Juanito$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996466143903316 996 $aHigher order logic theorem proving and its applications$91381960 997 $aUNISA