{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":3,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":65,"n_cols":5,"rows_kept":65,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[2,4,2,5],[3,2,3,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[9,2,9,3],[11,2,11,3],[11,4,11,5],[12,2,12,3],[12,4,12,5],[13,2,13,3],[13,4,13,5],[14,2,14,3],[15,2,15,3],[18,2,18,3],[19,2,19,3],[21,2,21,3],[23,2,23,3],[24,2,24,3],[28,2,28,3],[36,2,36,3],[36,4,36,5],[37,2,37,3],[37,4,37,5],[38,2,38,3],[39,2,39,3],[42,2,42,3],[43,2,43,3],[44,2,44,3],[45,2,45,3],[46,2,46,3],[57,2,57,3],[58,2,58,3],[62,2,62,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNISALENTO991002229429707536"]
[null,null,"Autore",null,"Boschi, Enzo"]
[null,null,"Titolo",null,"Catalogo dei forti terremoti in Italia dal 461 a. C. al 1980 / Enzo Boschi ... [et al.]"]
[null,null,"Pubbl/distr/stampa",null,"Istituto nazionale di geofisica ; Bologna : SGA, c1995"]
[null,null,"ISBN",null,"8885213073"]
[null,null,"Descrizione fisica",null,"973 p. ; 29 cm"]
[null,null,"Disciplina",null,"551.220945"]
[null,null,"Soggetti",null,"Terremoti - Italia - Storia"]
[null,null,"Lingua di pubblicazione",null,"Italiano"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,"2.","Record Nr.",null,"UNINA9910784526503321"]
[null,null,"Autore",null,"Poli C. <1935->"]
[null,null,"Titolo",null,"Design for manufacturing [[electronic resource] ] : a structured approach / / Corrado Poli"]
[null,null,"Pubbl/distr/stampa",null,"Boston, : Butterworth-Heinemann, c2001"]
[null,null,"ISBN",null,"1-283-28136-8"]
[{"$nulls":4},"9786613281364"]
[{"$nulls":4},"0-08-050394-2"]
[null,null,"Descrizione fisica",null,"1 online resource (409 p.)"]
[null,null,"Disciplina",null,"620/.0042 21"]
[{"$nulls":4},"670"]
[null,null,"Soggetti",null,"Engineering design"]
[{"$nulls":4},"Industrial design"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Note generali","Description based upon print version of record."]
[null,null,null,"Nota di bibliografia","Includes bibliographical references and index."]
[null,null,"Nota di contenuto",null,"Front Cover; Design for Manufacturing: A Structured Approach; Copyright Page; Contents; List of Figures; List of Tables; Preface; Acknowledgments; Responsibilities of Users; Chapter 1. Introduction; 1.1 Manufacturing, Design, and Design for Manufacturing; 1.2 Functional Designed Objects; 1.3 The Product Realization Process; 1.4 Industrial (or Product) Design; 1.5 Engineering Design; 1.6 Production Design; 1.7 Scope of the Book; 1.8 Summary; References; Questions and Problems; Chapter 2. Tolerances, Mechanical Properties, Physical Properties-A Review; 2.1 Interchangeability of Parts"]
[{"$nulls":4},"2.2 Tolerances2.3 Mechanical and Physical Properties; 2.4 Physical Properties of Materials; 2.5 Summary; References; Questions and Problems; Chapter 3. Polymer Processing; 3.1 The Processes; 3.2 Materials Used in Polymer Processing; 3.3 Injection Molding; 3.4 Compression Molding; 3.5 Transfer Molding; 3.6 Extrusion; 3.7 Extrusion Blow Molding; 3.8 Other Polymer Processes; 3.9 Qualitative DFM Guidelines for Injection Molding, Compression Molding, and Transfer Molding; 3.10 Summary; References; Questions and Problems; Chapter 4. Injection Molding: Relative Tooling Cost; 4.1 Introduction"]
[{"$nulls":4},"4.2 Estimating Relative Tooling Costs for Injection-Molded Parts4.3 Determining Relative Tooling Construction Costs Due to Basic Part Complexity (Cb); 4.4 Determining Cs; 4.5 Determining Ct; 4.6 Using the Part Coding System to Determine Cb, Cs, and Ct; 4.7 Total Relative "]
[{"$nulls":4},"Tooling Construction Cost; 4.8 Relative Mold Material Cost; 4.9 Multiple Cavity Molds; 4.10 Example 1-Relative Tooling Cost for a Simple Part; 4.11 Example 2-Relative Tooling Cost for a Complex Part; 4.12 Worksheet for Relative Tooling Cost; 4.13 Summary; References; Questions and Problems"]
[{"$nulls":4},"Appendix 4.A Notes for Figures 4.1 and 4.19, and Tables 4.1 and 4.2Appendix 4.B Worksheet for Relative Tooling Costs- Injection Molding; Chapter 5. Injection Molding: Total Relative Part Cost; 5.1 Injection Molded Part Costs; 5.2 Determining Total Relative Cycle Time (tr) for Injection-Molded Parts-Overview; 5.3 Determining the Basic Part Type: The First Digit; 5.4 Partitioning Partitionable Parts; 5.5 Non-Partitionable Parts; 5.6 Other Features Needed to Determine the First Digit; 5.7 Wall Thickness-The Second Digit; 5.8 Inserts and Internal Threadsn-The Third Digit"]
[{"$nulls":4},"5.9 Surface Requirements and TolerancesmThe Fourth and Fifth Digits5.10 Using the Coding System--Overview; 5.11 Effect of Materials on Relative Cycle Time; 5.12 Example 5.1-Determination of Relative Cycle Time for a Partitionable Part; 5.13 Example 5.2-Determination of Relative Cycle Time for a Partitionable Part; 5.14 Example 5.3-Determination of Relative Cycle Time for a Non-Partitionable Part; 5.15 Relative Processing Cost; 5.16 Relative Material Cost; 5.17 Total Relative Part Cost; 5.18 Example 5.4--Determination of the Total Relative Part Cost"]
[{"$nulls":4},"5.19 Worksheet for Relative Processing Cost and Total Relative Part Cost"]
[null,null,null,"Sommario/riassunto","Design for Manufacturing assists anyone not familiar with various manufacturing processes in better visualizing and understanding the relationship between part design and the ease or difficulty of producing the part.Decisions made during the early conceptual stages of design have a great effect on subsequent stages.  In fact, quite often more than 70% of the manufacturing cost of a product is determined at this conceptual stage, yet manufacturing is not involved. Through this book, designers will gain insight that will allow them to assess the impact of their proposed design on manufac"]
[null,"3.","Record Nr.",null,"UNINA9910767567003321"]
[null,null,"Titolo",null,"Theorem Proving in Higher Order Logics : 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14-18, 2000 Proceedings / / edited by Mark Aagaard, John Harrison"]
[null,null,"Pubbl/distr/stampa",null,"Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000"]
[null,null,"ISBN",null,"1-280-95654-2"]
[{"$nulls":4},"9786610956548"]
[{"$nulls":4},"3-540-44659-1"]
[null,null,"Edizione",null,"[1st ed. 2000.]"]
[null,null,"Descrizione fisica",null,"1 online resource (545 p.)"]
[null,null,"Collana",null,"Lecture Notes in Computer Science, , 1611-3349 ; ; 1869"]
[null,null,"Disciplina",null,"004.015113"]
[null,null,"Soggetti",null,"Artificial intelligence"]
[{"$nulls":4},"Computer science"]
[{"$nulls":4},"Compilers (Computer programs)"]
[{"$nulls":4},"Machine theory"]
[{"$nulls":4},"Software engineering"]
[{"$nulls":4},"Artificial Intelligence"]
[{"$nulls":4},"Theory of Computation"]
[{"$nulls":4},"Compilers and Interpreters"]
[{"$nulls":4},"Formal Languages and Automata Theory"]
[{"$nulls":4},"Computer Science Logic and Foundations of Programming"]
[{"$nulls":4},"Software Engineering"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Note generali","Description based upon print version of record."]
[null,null,null,"Nota di bibliografia","Includes bibliographical references and index."]
[null,null,"Nota di contenuto",null,"Fix-Point Equations for Well-Founded Recursion in Type Theory -- Programming and Computing in HOL -- Proof Terms for Simply Typed Higher Order Logic -- Routing Information Protocol in HOL/SPIN -- Recursive Families of Inductive Types -- Aircraft Trajectory Modeling and Alerting Algorithm Verification -- Intel’s Formal Verification Experience on the Willamette Development -- A Prototype Proof Translator from HOL to Coq -- Proving ML Type Soundness Within Coq -- On the Mechanization of Real Analysis in Isabelle/HOL -- Equational Reasoning via Partial Reflection -- Reachability Programming in HOL98 Using BDDs -- Transcendental Functions and Continuity Checking in PVS -- Verified Optimizations for the Intel IA-64 Architecture -- Formal "]
[{"$nulls":4},"Verification of IA-64 Division Algorithms -- Fast Tactic-Based Theorem Proving -- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover -- A Strong and Mechanizable Grand Logic -- Inheritance in Higher Order Logic: Modeling and Reasoning -- Total-Correctness Refinement for Sequential Reactive Systems -- Divider Circuit Verification with Model Checking and Theorem Proving -- Specification and Verification of a Steam-Boiler with Signal-Coq -- Functional Procedures in Higher-Order Logic -- Formalizing Stålmarck’s Algorithm in Coq -- TAS — A Generic Window Inference System -- Weak Alternating Automata in Isabelle/HOL -- Graphical Theories of Interactive Systems: Can a Proof Assistant Help? -- Formal Verification of the Alpha 21364 Network Protocol -- Dependently Typed Records for Representing Mathematical Structure -- Towards a Machine-Checked Java Specification Book -- Another Look at Nested Recursion -- Automating the Search for Answers to Open Questions -- Appendix: Conjectures Concerning Proof, Design, and Verification."]
[null,null,null,"Sommario/riassunto","This volume is the proceedings of the 13th International Conference on Theo­ rem Proving in Higher Order Logics (TPHOLs 2000) held 14-18 August 2000 in Portland, Oregon, USA. Each of the 55 papers submitted in the full rese­ arch category was refereed by at least three reviewers who were selected by the program committee. Because of the limited space available in the program and proceedings, only 29 papers were accepted for presentation and publication in this volume. In keeping with tradition, TPHOLs 2000 also offered a venue for the presen­ tation of work in progress, where researchers invite discussion by means of a brief preliminary talk and then discuss their work at a poster session. A supplemen­ tary proceedings containing associated papers for work in progress was published by the Oregon Graduate Institute (OGI) as technical report CSE-00-009. The organizers are grateful to Bob Colwell, Robin Milner and Larry Wos for agreeing to give invited talks. Bob Colwell was the lead architect on the Intel P6 microarchitecture, which introduced a number of innovative techniques and achieved enormous commercial success. As such, he is ideally placed to offer an industrial perspective on the challenges for formal verification. Robin Milner contributed many key ideas to computer theorem proving, and to functional programming, through his leadership of the influential Edinburgh LCF project."]