{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":2,"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":42,"n_cols":5,"rows_kept":42,"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],[5,2,5,3],[6,2,6,3],[7,2,7,3],[10,2,10,3],[11,2,11,3],[16,2,16,3],[16,4,16,5],[17,2,17,3],[17,4,17,5],[18,2,18,3],[19,2,19,3],[20,2,20,3],[21,2,21,3],[22,2,22,3],[23,2,23,3],[24,2,24,3],[36,2,36,3],[37,2,37,3],[39,2,39,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNINA9910707450303321"]
[null,null,"Autore",null,"Dibblee T. W (Thomas Wilson), <1911-2004, >"]
[null,null,"Titolo",null,"Geology of the Rogers Lake and Kramer quadrangles, California / / Thomas W. Dibblee"]
[null,null,"Pubbl/distr/stampa",null,"Washington, D.C. : , : United States Department of the Interior, Geological Survey, , 1960"]
[{"$nulls":4},"Washington, D.C. : , : Government Printing Office"]
[null,null,"Descrizione fisica",null,"1 online resource (73-139 pages, 3 pages of plates) : illustrations, maps, charts"]
[null,null,"Collana",null,"Geological Survey bulletin ; ; 1089-B"]
[null,null,"Soggetti",null,"Geology - California - Kern County"]
[{"$nulls":4},"Geology - California - San Bernardino County"]
[{"$nulls":4},"Geology - California - Los Angeles County"]
[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","Additional title page description: \"A study of an area in the central part of the western Mojave Desert.\""]
[{"$nulls":4},"Title from title screen (viewed July 23, 2014)."]
[null,null,null,"Nota di bibliografia","Includes bibliographical references (page 136) and index."]
[null,"2.","Record Nr.",null,"UNINA9910409661703321"]
[null,null,"Titolo",null,"Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I / / edited by Nicolas Peltier, Viorica Sofronie-Stokkermans"]
[null,null,"Pubbl/distr/stampa",null,"Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020"]
[null,null,"ISBN",null,"3-030-51074-3"]
[null,null,"Edizione",null,"[1st ed. 2020.]"]
[null,null,"Descrizione fisica",null,"1 online resource (553 pages)"]
[null,null,"Collana",null,"Lecture Notes in Artificial Intelligence, , 2945-9141 ; ; 12166"]
[null,null,"Disciplina",null,"006.3"]
[null,null,"Soggetti",null,"Machine theory"]
[{"$nulls":4},"Artificial intelligence"]
[{"$nulls":4},"Computer science"]
[{"$nulls":4},"Software engineering"]
[{"$nulls":4},"Compilers (Computer programs)"]
[{"$nulls":4},"Computer programming"]
[{"$nulls":4},"Formal Languages and Automata Theory"]
[{"$nulls":4},"Artificial Intelligence"]
[{"$nulls":4},"Computer Science Logic and Foundations of Programming"]
[{"$nulls":4},"Software Engineering"]
[{"$nulls":4},"Compilers and Interpreters"]
[{"$nulls":4},"Programming Techniques"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,"Nota di contenuto",null,"Invited Paper -- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints -- SAT; SMT and QBF -- An SMT Theory of Fixed-Point Arithmetic -- Covered Clauses Are Not Propagation Redundant -- The Resolution of Keller’s Conjecture -- How QBF Expansion Makes Strategy Extraction Hard -- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates -- Solving bit-vectors with MCSAT: explanations from bits and pieces -- Monadic Decomposition in Integer Linear Arithmetic -- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis -- Decision Procedures and Combination of Theories -- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols -- Combined Covers and Beth Definability -- "]
[{"$nulls":4},"Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates -- A Decision Procedure for String to Code Point Conversion -- Politeness for The Theory of Algebraic Datatypes -- Superposition -- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations -- A Combinator-Based Superposition Calculus for Higher-Order Logic -- Subsumption Demodulation in First-Order Theorem Proving -- A Comprehensive Framework for Saturation Theorem Proving -- Proof Procedures -- Possible Models Computation and Revision - A Practical Approach -- SGGS Decision Procedures -- Integrating Induction and Coinduction via Closure Operators and Proof Cycles -- Logic-Independent Proof Search in Logical Frameworks (short paper) -- Layered Clause Selection for Theory Reasoning (short paper) -- Non Classical Logics -- Description Logics with Concrete Domains and General Concept Inclusions Revisited -- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic -- Constructive Hybrid Games -- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) -- NP Reasoning in the Monotone µ-Calculus -- Soft subexponentials and multiplexing -- Mechanised Modal Model Theory."]
[null,null,null,"Sommario/riassunto","This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods). The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics: Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools *The conference was held virtually due to the COVID-19 pandemic. Chapter ‘Constructive Hybrid Games’ is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com."]