02916oam 2200637Mn 450 991078756990332120211215042403.00-429-16800-41-4665-8825-X10.1201/b16118 (CKB)2670000000394810(EBL)1408050(SSID)ssj0001140669(PQKBManifestationID)11993279(PQKBTitleCode)TC0001140669(PQKBWorkID)11240076(PQKB)11462565(MiAaPQ)EBC1408050(OCoLC)868795684(OCoLC)1140431710(OCoLC-P)1140431710(FlBoTFG)9780429168000(OCoLC)1058331353(OCoLC-P)1058331353(CaSebORM)9781466588257(EXLCZ)99267000000039481020190103d2017 uy 0engur|n|||||||||txtccrDictionary of oil, gas, and petrochemical processing[Place of publication not identified]CRC Press20171 online resource (480 p.)Description based upon print version of record.1-138-43450-7 1-4665-8826-8 Front Cover; Preface; Authors; Chapter 1: A; Chapter 2: B; Chapter 3: C; Chapter 4: D; Chapter 5: E; Chapter 6: F; Chapter 7: G; Chapter 8: H; Chapter 9: I; Chapter 10: J; Chapter 11: K; Chapter 12: L; Chapter 13: M; Chapter 14: N; Chapter 15: O; Chapter 16: P; Chapter 17: Q; Chapter 18: R; Chapter 19: S; Chapter 20: T; Chapter 21: U; Chapter 22: V; Chapter 23: W; Chapter 24: X; Chapter 25: Y; Chapter 26: Z; Back CoverIn industry, miscommunication can cause frustration, create downtime, and even trigger equipment failure. By providing a common ground for more effective discourse, the Dictionary of Oil, Gas, and Petrochemical Processing can help eliminate costly miscommunication.An essential resource for oil, gas, and petrochemical industry professionals, engineers, academic staff, and science and engineering students, the dictionary defines over 5,000 technical and commercial terms encompassing exploration, production, processing, refining, pipelining, finance, management, and safety. From Petroleum industry and tradeDictionariesPetroleum engineeringDictionariesGas manufacture and worksDictionariesPetroleumRefiningDictionariesPetroleum industry and tradePetroleum engineeringGas manufacture and worksPetroleumRefining480BAHADORI ALIREZA877892OCoLC-POCoLC-PBOOK9910787569903321Dictionary of oil, gas, and petrochemical processing3805405UNINA05557nam 22008175 450 991048367680332120251226195910.03-642-39634-810.1007/978-3-642-39634-2(CKB)3710000000002639(SSID)ssj0000962843(PQKBManifestationID)11573006(PQKBTitleCode)TC0000962843(PQKBWorkID)10976365(PQKB)10061076(DE-He213)978-3-642-39634-2(MiAaPQ)EBC3101196(PPN)172428416(EXLCZ)99371000000000263920130722d2013 u| 0engurnn|008mamaatxtccrInteractive Theorem Proving 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings /edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie1st ed. 2013.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2013.1 online resource (XII, 498 p. 73 illus.) Theoretical Computer Science and General Issues,2512-2029 ;7998Bibliographic Level Mode of Issuance: Monograph3-642-39633-X Includes bibliographical references and index.Invited Talks -- Applying Formal Methods in the Large -- Automating Theorem Proving with SMT -- Certifying Voting Protocols -- Invited Tutorials.-Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities -- Canonical Structures for the Working Coq User -- Regular Papers -- MaSh: Machine Learning for Sledgehammer -- Scalable LCF-Style Proof Translation -- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation -- Automatic Data Refinement -- Data Refinement in Isabelle/HOL -- Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable -- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1 -- Mechanising Turing Machines and Computability Theory in Isabelle/HOL.-A Machine-Checked Proof of the Odd Order Theorem -- Kleene Algebra with Tests and Coq Tools for while Programs.-Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL -- Pragmatic Quotient Types in Coq -- Mechanical Verification of SAT Refutations with Extended Resolution -- Formalizing Bounded Increase -- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types -- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL -- Formal Reasoning about Classified Markov Chains in HOL -- Practical Probability: Applying pGCL to Lattice Scheduling -- Adjustable References -- Handcrafted Inversions Made Operational on Operational Semantics -- Circular Coinduction in Coq Using Bisimulation-Up-To Techniques -- Program Extraction from Nested Definitions -- Subformula Linking as an Interaction Method -- Automatically Generated Infrastructure for De Bruijn Syntaxes -- Shared-Memory Multiprocessing for Interactive Theorem Proving -- A Parallelized Theorem Prover for a Logic with Parallel Execution -- Rough Diamonds -- Communicating Formal Proofs: The Case of Flyspeck -- Square Root and Division Elimination in PVS -- The Picard Algorithm for Ordinary Differential Equations in Coq -- Stateless Higher-OrderLogic with Quantified Types -- Implementing Hash-Consed Structures in Coq -- Towards Certifying Network Calculus -- Steps towards Verified Implementations of HOL Light.This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.Theoretical Computer Science and General Issues,2512-2029 ;7998Machine theoryArtificial intelligenceComputer scienceSoftware engineeringData protectionAlgorithmsFormal Languages and Automata TheoryArtificial IntelligenceComputer Science Logic and Foundations of ProgrammingSoftware EngineeringData and Information SecurityAlgorithmsMachine theory.Artificial intelligence.Computer science.Software engineering.Data protection.Algorithms.Formal Languages and Automata Theory.Artificial Intelligence.Computer Science Logic and Foundations of Programming.Software Engineering.Data and Information Security.Algorithms.004.015113Blazy Sandrineedthttp://id.loc.gov/vocabulary/relators/edtPaulin-Mohring Christineedthttp://id.loc.gov/vocabulary/relators/edtPichardie Davidedthttp://id.loc.gov/vocabulary/relators/edtMiAaPQMiAaPQMiAaPQBOOK9910483676803321Interactive Theorem Proving2010767UNINA