{"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":55,"n_cols":5,"rows_kept":55,"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],[11,2,11,3],[12,2,12,3],[17,2,17,3],[17,4,17,5],[18,2,18,3],[18,4,18,5],[19,2,19,3],[21,2,21,3],[22,2,22,3],[23,2,23,3],[24,2,24,3],[25,2,25,3],[26,2,26,3],[27,2,27,3],[29,2,29,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],[40,2,40,3],[42,2,42,3],[50,2,50,3],[51,2,51,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNINA9910466580903321"]
[null,null,"Autore",null,"Harding Sue-Ann"]
[null,null,"Titolo",null,"Beslan : six stories of the siege / / Sue-Ann Harding"]
[null,null,"Pubbl/distr/stampa",null,"Manchester, England : , : Manchester University Press, , 2012"]
[null,null,"ISBN",null,"1-5261-3021-1"]
[null,null,"Descrizione fisica",null,"1 online resource (259 p.) : ill"]
[null,null,"Disciplina",null,"363.3250947"]
[null,null,"Soggetti",null,"Beslan Massacre, Beslan, Russia, 2004"]
[{"$nulls":4},"Terrorism - Russia (Federation) - Beslan"]
[{"$nulls":4},"Terrorism"]
[{"$nulls":4},"Electronic books."]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Nota di bibliografia","Includes bibliographical references (pages [231]-244) and index."]
[null,null,null,"Sommario/riassunto","This book is the first, sustained close reading of Russian-language online media accounts of the 2004 Beslan school siege, now seen as a vital turning point in Russia's approach to terrorism and in the Putin/Medvedev presidencies. It investigates the reportage of the hostage-taking published by three very different websites: RIA-Novosti, a large, Russian state-controlled news agency; Kavkazcenter, the major site of the Chechen armed resistance; and Caucasian Knot, founded by Memorial, the internationally acclaimed Russian human rights NGO. By tracking the ways in which these three sites constructed six different reports relating, and responding to, what happened at Beslan, even as events were still taking place, this book is an investigation of material that has never before been subjected to scholarly analysis in this depth and to such a systematic degree. By covering both Russian and English reports, the book also considers issues of translation, particularly in regard to online publishing, and ways in which translation impacts on the reconstruction of these narratives. Working from the premises that narratives do not merely represent but constitute reality, are fundamental to human agency, and are used to account for, legitimise, and challenge behaviour and the practices of institutions, the book also reflects on the potential for certain kinds of narratives to either perpetuate or dissolve violent political conflict, a discussion that is relevant not just for Beslan and for Russia, but for those involved in other violent, seemingly intractable, conflicts across the world, and for "]
[{"$nulls":4},"those who would undo them."]
[null,"2.","Record Nr.",null,"UNISA996464426903316"]
[null,null,"Titolo",null,"Intelligent computer mathematics : 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings / / Fairouz Kamareddine, Claudio Sacerdoti Coen (editors)"]
[null,null,"Pubbl/distr/stampa",null,"Cham, Switzerland : , : Springer, , [2021]"]
[{"$nulls":4},"©2021"]
[null,null,"ISBN",null,"3-030-81097-6"]
[null,null,"Descrizione fisica",null,"1 online resource (263 pages)"]
[null,null,"Collana",null,"Lecture notes in computer science ; ; 12833"]
[null,null,"Disciplina",null,"004.0151"]
[null,null,"Soggetti",null,"Computer science - Mathematics"]
[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,"Intro -- Preface -- Organization -- Invited Talks -- Logics at Work, and Some Challenges for Computer Mathematics -- Induction in Saturation-Based Reasoning -- Doing Number Theory in Weak Systems of Arithmetic -- Contents -- Formalizations -- A Modular First Formalisation of Combinatorial Design Theory -- 1 Introduction -- 2 Background -- 2.1 Mathematical Background -- 2.2 Isabelle and Locales -- 3 The Basic Design Formalisation -- 3.1 Pre-designs -- 3.2 Basic Design Properties -- 3.3 Basic Design Operations -- 4 The Block Design Hierarchy -- 4.1 Restricting Block Size -- 4.2 Balanced Designs -- 4.3 T-Designs -- 4.4 Uniform Replication Number -- 4.5 BIBDs and Proofs -- 4.6 BIBD Extensions -- 5 Extending the Formalisation -- 5.1 Resolvable Designs -- 5.2 Group Divisible Designs -- 5.3 Design Isomorphisms -- 5.4 Graph Theory -- 6 The Modular Approach -- 6.1 The Formal Design Hierarchy -- 6.2 The Little Theories Approach -- 6.3 Notational Benefits -- 6.4 Reasoning on Locales -- 6.5 Limitations -- 7 Conclusion and Future Work -- References -- Beautiful Formalizations in Isabelle/Naproche -- 1 Introduction -- 2 Naproche, ForTheL, and LaTeX -- 3 Example: Cantor's Theorem -- 4 Example: König's Theorem -- 5 Example: Euclid's Theorem -- 6 Example: Furstenberg's Topological Proof -- 7 Example: The Knaster-Tarski Theorem -- 8 Outlook -- References -- Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL -- 1 Introduction -- 2 Related Work -- 3 Implication and Falsity -- 3.1 Language -- 3.2 Wajsberg 1937 -- 3.3 Wajsberg 1939 -- 3.4 Shortest Axiom -- 4 Disjunction and Negation -- 4.1 Language -- 4.2 Rasiowa 1949 -- 4.3 Russell "]
[{"$nulls":4},"1908 and Bernays 1926 -- 4.4 Whitehead and Russell 1910 -- 5 Challenges and Benefits -- 6 Conclusion -- References -- Formalization of RBD-Based Cause Consequence Analysis in HOL -- 1 Introduction -- 2 Preliminaries."]
[{"$nulls":4},"2.1 RBD Formalization -- 2.2 ET Formalization -- 3 Cause-Consequence Diagram Formalization -- 3.1 Formal CCD Modeling -- 3.2 Formal CCD Analysis -- 4 Conclusion -- References -- Automatic Theorem Proving and Machine Learning -- Online Machine Learning Techniques for Coq: A Comparison -- 1 Introduction -- 1.1 Contributions -- 2 Tactic and Proof State Representation -- 3 Prediction Models -- 3.1 Locality Sensitive Hashing Forests for Online k-NN -- 3.2 Online Random Forest -- 3.3 Boosted Trees -- 4 Experimental Evaluation -- 4.1 Split Evaluation -- 4.2 Chronological Evaluation -- 4.3 Evaluation in Tactician -- 4.4 Feature Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Improving Stateful Premise Selection with Transformers -- 1 Introduction -- 2 Data -- 3 Experiments -- 4 Conclusion and Future Work -- References -- Towards Math Terms Disambiguation Using Machine Learning -- 1 Introduction -- 2 Related Works -- 2.1 The DLMF Dataset -- 2.2 Part-of-Math Tagger -- 2.3 Word Sense Disambiguation in NLP -- 2.4 Machine Learning Models -- 2.5 Math Language Processing -- 3 The Dataset -- 4 Machine Learning Approach -- 4.1 Data Prepossessing -- 4.2 Feature Engineering -- 4.3 Training the Models -- 4.4 Evaluation Metric -- 5 Results -- 5.1 Gamma -- 5.2 Prime -- 5.3 Superscript -- 6 Conclusion and Future Work -- References -- Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving -- 1 Introduction -- 2 Hyper-Parameter Optimisation -- 3 Heterogeneous Heuristic Optimisation and Scheduling -- 4 Heuristic Optimisation for Heterogeneous Instances -- 4.1 Dynamic Evaluation Clustering -- 4.2 Local Heuristic Optimisation -- 4.3 Embedding Unsolved Problems -- 5 Local Schedules for Heterogeneous Instances -- 6 Schedule Selection -- 7 Experimental Evaluation -- 7.1 Discovering New Heuristics."]
[{"$nulls":4},"7.2 Revealing Homogeneity with Admissible Evaluation Clustering -- 7.3 Embedding Evaluation Features -- 7.4 Optimal Scheduling of Heuristics -- 7.5 Overall Performance Contribution -- 8 Conclusion -- References -- Inductive Benchmarks for Automated Reasoning -- 1 Introduction -- 2 Benchmark Format -- 3 Benchmark Categories -- 3.1 dty - Benchmarks with Inductively Defined Data Types -- 3.2 int - Benchmarks with Integers -- 4 Conclusions -- References -- A Heuristic Prover for Elementary Analysis in Theorema -- 1 Introduction -- 2 Application of Special Techniques -- 3 Conclusion and Further Work -- References -- Search and Classification -- Searching for Mathematical Formulas Based on Graph Representation Learning -- 1 Introduction -- 2 Related Work -- 3 Graph Representation for Mathematical Formula -- 4 Formula Embedding Model -- 4.1 Self-supervised Learning Tasks -- 4.2 Graph Neural Networks -- 4.3 Hyperparameter Choices -- 5 Experiments and Evaluation -- 5.1 Evaluation Metric -- 5.2 Evaluation Results -- 6 Conclusion and Future Work -- References -- 10 Years Later: The Mathematics Subject Classification and Linked Open Data -- 1 Introduction -- 2 MSC 2020 SKOSification -- 2.1 Reasons for a New Version -- 3 Conclusion and Future Work -- References -- WebMIaS on Docker -- 1 Introduction -- 2 Deployment Process Description -- 3 Evaluation -- 4 Conclusion -- References -- Teaching and Geometric Reasoning -- Learning to Solve Geometric Construction Problems from Images -- 1 Introduction -- 2 Related Work -- 3 Our Euclidea Geometric Construction Environment -- 4 Supervised Visual Learning Approach -- 4.1 Action to Mask: Generating Training Data -- 4.2 Mask to Action: Converting Output "]
[{"$nulls":4},"Masks to Euclidea Actions -- 4.3 Solving Construction Problems by Sequences of Actions -- 4.4 Additional Components of the Approach."]
[{"$nulls":4},"5 Solving Unseen Geometric Problems via Hypothesis Tree Search -- 5.1 Generating Action Hypotheses -- 5.2 Tree Search for Exploring Construction Hypotheses -- 6 Experiments -- 6.1 Benefits of Different Components of Our Approach -- 6.2 Evaluation of the Supervised Learning Approach -- 6.3 Evaluation on Unseen Problems -- 6.4 Qualitative Example -- 7 Conclusion -- References -- Automated Generation of Exam Sheets for Automated Deduction -- 1 Motivation -- 2 Random Problem Generation -- 2.1 Boolean Satisfiability (SAT) -- 2.2 Non-ground Superposition with Redundancy -- 3 Random Variation of Problem Templates -- 3.1 Satisfiability Modulo Theories (SMT) -- 3.2 Ground Superposition -- 4 Implementation -- 5 Evaluation of Online Exam Outcomes -- 6 Conclusion -- References -- Gauss-Lintel, an Algorithm Suite for Exploring Chord Diagrams -- 1 Gauss Diagrams and Their Properties -- 2 Even-Odd Matchings and Lintels -- 3 Implementation -- 3.1 Lintel Generation and Canonization -- 3.2 Properties/Conditions Checking -- 4 Experiments and Results -- 5 Related Work -- References -- Logic and Systems -- A New Export of the Mizar Mathematical Library -- 1 Introduction -- 2 Design -- 2.1 Formalizing the Mizar Logic -- 2.2 Exporting the MML as XML -- 2.3 Reading the XML into Scala Classes -- 2.4 Translating the Scala Classes to MMT -- 3 Conclusion and Future Work -- References -- A Language with Type-Dependent Equality -- 1 Introduction -- 2 Motivating Considerations and Related Work -- 2.1 Type-Dependent Equality -- 2.2 Abstract Definitions and Quotient Types -- 2.3 Predicate and Quotient Types -- 2.4 Records and Predicate/Quotient Types -- 3 Formal Language Definition -- 3.1 Syntax and Inference System -- 3.2 Semantics -- 3.3 Lax Record Types -- 4 Conclusion -- References -- Generating Custom Set Theories with Non-set Structured Objects -- 1 Introduction."]
[{"$nulls":4},"2 Logical Framework -- 3 Example Axiomatizations of Generalized Set Theories -- 4 Model Building Kit -- 5 Connecting Models to Domains -- 6 Examples of Models of GSTs -- 7 Conclusion and Future Work -- References -- CICM'21 Systems Entries -- References -- Author Index."]
[null,"3.","Record Nr.",null,"UNINA9910146777803321"]
[null,null,"Titolo",null,"Nanobiotechnology : the journal at the intersection of nanotechnology, molecular biology, and biomedical sciences"]
[null,null,"Pubbl/distr/stampa",null,"[Totowa, N.J.], : Humana Press"]
[null,null,"ISSN",null,"1551-1294"]
[null,null,"Disciplina",null,"620"]
[{"$nulls":4},"660.6"]
[null,null,"Soggetti",null,"Biotechnology"]
[{"$nulls":4},"Nanotechnology"]
[{"$nulls":4},"Molecular biology"]
[{"$nulls":4},"Molecular Biology"]
[{"$nulls":4},"Biotechnologie"]
[{"$nulls":4},"Biologie moléculaire"]
[{"$nulls":4},"Periodical"]
[{"$nulls":4},"Periodicals."]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Periodico"]
[null,null,null,"Note generali","Refereed/Peer-reviewed"]
[{"$nulls":4},"Title from journal information screen (FirstSearch, viewed Sept. 7, 2006)."]