LEADER 05873nam 22008175 450 001 996465430403316 005 20200706163114.0 010 $a3-540-30142-9 024 7 $a10.1007/b100400 035 $a(CKB)1000000000212544 035 $a(SSID)ssj0000257939 035 $a(PQKBManifestationID)11194622 035 $a(PQKBTitleCode)TC0000257939 035 $a(PQKBWorkID)10253744 035 $a(PQKB)11728063 035 $a(DE-He213)978-3-540-30142-4 035 $a(MiAaPQ)EBC3087845 035 $a(PPN)155210661 035 $a(EXLCZ)991000000000212544 100 $a20121227d2004 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] $e17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings /$fedited by Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan 205 $a1st ed. 2004. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2004. 215 $a1 online resource (VIII, 340 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v3223 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-23017-3 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aError Analysis of Digital Filters Using Theorem Proving -- Verifying Uniqueness in a Logical Framework -- A Program Logic for Resource Verification -- Proof Reuse with Extended Inductive Types -- Hierarchical Reflection -- Correct Embedded Computing Futures -- Higher Order Rippling in IsaPlanner -- A Mechanical Proof of the Cook-Levin Theorem -- Formalizing the Proof of the Kepler Conjecture -- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code -- Extensible Hierarchical Tactic Construction in a Logical Framework -- Theorem Reuse by Proof Term Transformation -- Proving Compatibility Using Refinement -- Java Program Verification via a JVM Deep Embedding in ACL2 -- Reasoning About CBV Functional Programs in Isabelle/HOL -- Proof Pearl: From Concrete to Functional Unparsing -- A Decision Procedure for Geometry in Coq -- Recursive Function Definition for Types with Binders -- Abstractions for Fault-Tolerant Distributed System Verification -- Formalizing Integration Theory with an Application to Probabilistic Algorithms -- Formalizing Java Dynamic Loading in HOL -- Certifying Machine Code Safety: Shallow Versus Deep Embedding -- Term Algebras with Length Function and Bounded Quantifier Alternation. 330 $aThis volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14?17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higher-order logics as well as related topics in theorem proving and veri?cation. There were 42 papers submitted to TPHOLs 2004 in the full research ca- gory, each of which was refereed by at least 3 reviewers selected by the program committee. Of these submissions, 21 were accepted for presentation at the c- ference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2004 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings c- taining papers about in-progress work was published as a 2004 technical report of the School of Computing at the University of Utah. The organizers are grateful to Al Davis, Thomas Hales, and Ken McMillan for agreeing to give invited talks at TPHOLs 2004. The TPHOLs conference traditionally changes continents each year in order to maximize the chances that researchers from around the world can attend. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v3223 606 $aArtificial intelligence 606 $aComputers 606 $aArchitecture, Computer 606 $aMathematical logic 606 $aComputer logic 606 $aSoftware engineering 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 615 0$aArtificial intelligence. 615 0$aComputers. 615 0$aArchitecture, Computer. 615 0$aMathematical logic. 615 0$aComputer logic. 615 0$aSoftware engineering. 615 14$aArtificial Intelligence. 615 24$aTheory of Computation. 615 24$aComputer System Implementation. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 676 $a511.36028563 702 $aSlind$b Konrad$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBunker$b Annette$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aGopalakrishnan$b Ganesh C$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465430403316 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNISA LEADER 05427nam 2200673 450 001 9910831032303321 005 20230721023316.0 010 $a1-283-37240-1 010 $a9786613372406 010 $a0-470-74483-9 010 $a0-470-74482-0 035 $a(CKB)1000000000820658 035 $a(EBL)698220 035 $a(OCoLC)813005391 035 $a(SSID)ssj0000354398 035 $a(PQKBManifestationID)11212582 035 $a(PQKBTitleCode)TC0000354398 035 $a(PQKBWorkID)10313210 035 $a(PQKB)11195513 035 $a(MiAaPQ)EBC698220 035 $a(EXLCZ)991000000000820658 100 $a20160808h20092009 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 00$aLCD backlights /$fedited by Shunsuke Kobayashi, Shigeo Mikoshiba, Sungkyoo Lim 210 1$aChichester, [England] :$cWiley,$d2009. 210 4$dİ2009 215 $a1 online resource (293 p.) 225 1 $aWiley-SID Series in Display Technology 300 $aDescription based upon print version of record. 311 $a0-470-69967-1 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aLCD Backlights; Contents; Series Editor's Foreword; About the Editors; List of Contributors; Preface; Part One: Backlights by Use; 1: Technical Trends and Requirements/Specifications for LCD TV Backlights; 1.1 Introduction; 1.2 Structure of LCD TV Backlights; 1.3 Trends in LCD TV Backlights; 1.4 Requirements/Specifications for LCD TV Backlights; 1.5 Conclusions; References; 2: Improvement of Moving Picture Quality by Means of Backlight Control; 2.1 Introduction; 2.2 Blur of Moving Images on LC Displays; 2.3 Methods of Reducing Motion Blur; 2.4 Backlight Blinking; 2.5 Conclusions; References 327 $a3: Multiple Primary Color Backlights3.1 Present Status; 3.2 Technological Impacts; 3.3 Operation of Prototype, Six-primary-color Monitor; 3.4 Details of a Six-primary-color Backlight Unit; 3.5 Signal Processing of Transforming from Three Primaries to Six Primaries; 3.6 Color Gamut of the Prototype Monitor; 3.7 Other Techniques for Multiple Primary Color LC-TVs; 3.8 Remaining Issues; References; 4: Reduction of Backlight Power Consumption of LCD-TVs; 4.1 Introduction; 4.2 Display Method of LCD and Power Reduction; 4.3 Principle of the Adaptive Dimming Technique 327 $a4.4 Adaptive Dimming Control and Power Consumption4.5 Other Features of the Adaptive Dimming Technique; References; 5: Notebook PC/Monitor Backlights; 5.1 Introduction; 5.2 Characteristics Required for Backlights; 5.3 Optical Systems for Backlights; 5.4 Light Sources for Backlights; 5.5 Optical Components of Backlights; References; 6: Backlights for Handheld Data Terminals; 6.1 Introduction; 6.2 Basic Structure and Principles of LED Backlights; 6.3 Constituents of LED BLUs; 6.4 Various LED Backlight Configurations; 6.5 Conclusions; References; Part Two: Light Source Devices 327 $a7: CCFL Backlights7.1 Introduction; 7.2 Structure and Operating Principle of CCFLs; 7.3 Basic Characteristics of CCFLs; 7.4 Future Trends in CCFLs; 7.5 Conclusions; 8: CCFL Inverters; 8.1 Introduction; 8.2 Various Drive Schemes of CCFL Inverters; 8.3 Equivalent Circuit of CCFLs; 8.4 Inverter Circuits; 8.5 Driving of CCFLs with Inverters; 8.6 Lamp Current Balancers for Driving Multiple Lamps; 8.7 Conclusions; References; 9: HCFL Backlights; 9.1 HCFL Light Source as a Member of the Fluorescent Lamp Family; 9.2 Introduction of the Hot Cathode in Fluorescent Lamps; 9.3 Driving the HCFL 327 $a9.4 Cathode Life Properties of HCFL9.5 Lumen Maintenance and Color Point Shift during Life; 9.6 Designing a Backlight with HCFL; 9.7 The Scanning Feature, Cost-effectively Enabled by HCFL; 9.8 The Dimming Feature; 9.9 Conclusions; References; 10: EEFL Backlights; 10.1 Introduction; 10.2 Basic Characteristics of EEFLs; 10.3 Advantages and Disadvantages of EEFL Backlights; 10.4 Technological Trends of EEFL Backlights; 10.5 Development Targets; 10.6 Conclusions; References; 11: FFL Backlights; 11.1 Introduction; 11.2 The History of FFL Development; 11.3 Characteristics of FFLs 327 $a11.4 Features of the FFL 330 $aResearch and development on liquid crystal display (LCD) backlight technologies are becoming increasingly important due to the fast growth of the LCD business. Backlight technologies contribute to functional improvements of LCDs in terms of wide colour reproduction, uniformity improvements of luminance and colour temperature, high luminance, long life, less power consumption, thinner backlight unit, as well as cost. As LCD panel technology progresses, the lighting technology that provides the illumination for the panel must similarly evolve. LCD Backlights is written by a global panel 410 0$aWiley SID series in display technology. 606 $aLiquid crystal displays$xEquipment and supplies 606 $aElectric lamps 615 0$aLiquid crystal displays$xEquipment and supplies. 615 0$aElectric lamps. 676 $a621.3815/422 676 $a621.3815422 702 $aKobayashi$b Shunsuke 702 $aMikoshiba$b Shigeo 702 $aLim$b Sungkyoo 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910831032303321 996 $aLCD backlights$93965855 997 $aUNINA