01067nam0-2200349---450-99001003405040332120160129104152.09788813339975001003405FED01001003405(Aleph)001003405FED0100100340520160129d----2015km-y0itay50------baitay---n---001yyCommentario breve al codice di procedura civileFederico Carpi - Vittorio Colesanti -Michele Taruffocon la collaborazione di Caterina Arrigoni ... [et al.]8. ed.PadovaCedam2015XCIX, 3726 p.24 cmBreviaria Iurisfondati da G.Cian e A.TrabucchiCodice di procedura civileCommentario347.0502648Carpi,FedericoColesanti,VittorioTaruffo,MicheleArrigoni,CaterinaITUNINARICAUNIMARCBK990010034050403321ZZa/82DDRCDDRCUNINA06725nam 22007335 450 99646643770331620200703132248.03-319-94205-010.1007/978-3-319-94205-6(CKB)4100000005323110(DE-He213)978-3-319-94205-6(MiAaPQ)EBC6296149(PPN)229502296(EXLCZ)99410000000532311020180629d2018 u| 0engurnn|008mamaatxtrdacontentcrdamediacrrdacarrierAutomated Reasoning[electronic resource] 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani1st ed. 2018.Cham :Springer International Publishing :Imprint: Springer,2018.1 online resource (XVI, 724 p. 128 illus.) Lecture Notes in Artificial Intelligence ;109003-319-94204-2 An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem -- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics -- Superposition for Lambda-Free Higher-Order Logic -- Automated Reasoning about Key Sets -- A Tableaux Calculus for Reducing Proof Size -- FORT 2.0 -- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover -- The Higher-Order Prover Leo-III -- Well-Founded Unions -- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories -- Cubicle-W: Parameterized Model Checking on Weak Memory -- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property -- A Why3 framework for reflection proofs and its application to GMP's algorithms -- Infinitely-valued Logic -- Uniform Substitution for Differential Game Logic -- A Logical Framework with Commutative and Non-Commutative Subexponentials -- Exploring Approximations for Floating-Point Arithmetic using UppSAT -- Complexity of Combinations of Qualitative Constraint Satisfaction Problems -- A Generic Framework for Implicate Generation Modulo Theories -- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems -- A New Probabilistic Algorithm for Approximate Model Counting -- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems -- Cops and CoCoWeb: Infrastructure for Conuence Tools -- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing -- Superposition with Datatypes and Codatatypes -- Efficient encodings of first-order Horn formulas in equational logic -- A FOOLish Encoding of the Next State Relations of Imperative Programs -- Constructive Decision via Redundancy-free Proof-Search -- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates -- A Separation Logic with Data: Small Models and Automation -- MaedMax: A Maximal Ordered Completion Tool -- From Syntactic Proofs to Combinatorial Proofs -- A Resolution-Based Calculus for Preferential Logics -- Extended Resolution Simulates DRAT -- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle -- Efficient Interpolation for the Theory of Arrays -- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback -- Theories as Types -- Datatypes with Shared Selectors -- Enumerating Justifications using Resolution -- A SAT-Based Approach to Learn Explainable Decision Sets -- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions -- An abstraction-refinement framework for reasoning with large theories -- Efficient Model Construction for Horn Logic with VLog: System Description -- Focussing, MALL and the polynomial hierarchy -- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.This book constitutes the refereed proceedings of the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, held in Oxford, United Kingdom, in July 2018, as part of the Federated Logic Conference, FLoC 2018. In 2018, IJCAR unites CADE, TABLEAUX, and FroCoS, the International Symposium on Frontiers of Combining Systems, and, for the fourth time, is part of the Federated Logic Conference. The 38 revised full research papers and 8 system descriptions presented together with two invited talks were carefully reviewed and selected from 108 submissions. The papers focus on topics such as logics, deductive systems, proof-search methods, theorem proving, model checking, verification, formal methods, and program analysis.Lecture Notes in Artificial Intelligence ;10900Mathematical logicArtificial intelligenceComputer logicAlgorithmsSoftware engineeringProgramming languages (Electronic computers)Mathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XAlgorithm Analysis and Problem Complexityhttps://scigraph.springernature.com/ontologies/product-market-codes/I16021Software Engineeringhttps://scigraph.springernature.com/ontologies/product-market-codes/I14029Programming Languages, Compilers, Interpretershttps://scigraph.springernature.com/ontologies/product-market-codes/I14037Mathematical logic.Artificial intelligence.Computer logic.Algorithms.Software engineering.Programming languages (Electronic computers).Mathematical Logic and Formal Languages.Artificial Intelligence.Logics and Meanings of Programs.Algorithm Analysis and Problem Complexity.Software Engineering.Programming Languages, Compilers, Interpreters.004.015113Galmiche Didieredthttp://id.loc.gov/vocabulary/relators/edtSchulz Stephanedthttp://id.loc.gov/vocabulary/relators/edtSebastiani Robertoedthttp://id.loc.gov/vocabulary/relators/edtMiAaPQMiAaPQMiAaPQBOOK996466437703316Automated Reasoning771895UNISA02315nam 2200337z- 450 991055741830332120231214141111.0(CKB)5400000000043511(oapen)https://directory.doabooks.org/handle/20.500.12854/78688(EXLCZ)99540000000004351120202202d2022 |y 0gerurmn|---annantxtrdacontentcrdamediacrrdacarrierDie Kunst zu lebenDie biographische Verarbeitung von Katastrophenerfahrungen und Emotionen von Künstlern im gegenwärtigen JapanUniversitätsverlag Göttingen20223-86395-518-8 Throughout the world, ‘3.11’ and ‘Fukushima’ are used as synonyms for catastrophe, despair and insecurity. In a search for sociocultural meaning in the catastrophic events of ‘3.11’, Wiebke Grimmig examines the role of contemporary Japanese artists in the process by which Japanese society has handled the effects of this triple disaster (earthquake, tsunami and atomic disaster) in Fukushima. She focuses on the emotional processing of these events by her respondents, including their biographical background, their economic concerns and the role of contemporary art in Japanese society. This anthropological research involves the analysis of in-depth interviews with contemporary artists from Tokyo, as well as from other locations along the east coast of Japan. This research was conducted over a 12-month period to elucidate the catastrophic events and effects of the ‘3.11’ disaster. In this work, Wiebke Grimmig examines how contemporary Japanese artists portray catastrophic events in terms of emotion, individuality, power, resilience, politics, economics and communication in their biographical narrative and their work. This doctoral thesis provides an important contribution to the socio-scientific field of disaster research.Kunst zu leben Society & social sciencesbicsscJapanartistemotional processingSociety & social sciencesGrimmig Wiebkeauth1302074BOOK9910557418303321Die Kunst zu leben3026099UNINA