LEADER 01029nam--2200349---450- 001 990002855890203316 005 20070116163751.0 035 $a000285589 035 $aUSA01000285589 035 $a(ALEPH)000285589USA01 035 $a000285589 100 $a20070116d1970----km-y0itay50------ba 101 $aita 102 $aIT 105 $a||||||||001yy 200 1 $a<> sicurezza sul lavoro e la prevenzione degli infortuni$enelle officine meccaniche$fMario Vignale 210 $aPisa$cEdizioni della Scuola di magistero tecnico$d1970 215 $a223 p.$d24 cm. 410 0$12001 454 1$12001 461 1$1001-------$12001 606 0 $aInfortuni sul lavoro$xPrevenzione 676 $a363.11967 700 1$aVIGNALE,$bMario$0226874 801 0$aIT$bsalbc$gISBD 912 $a990002855890203316 951 $aII/40$b496$cII 959 $aBK 969 $aDIMEC 979 $aDIMEC$b90$c20070116$lUSA01$h1637 996 $aSicurezza sul lavoro e la prevenzione degli infortuni$9991838 997 $aUNISA LEADER 06225nam 22007575 450 001 9910349422303321 005 20251225202143.0 010 $a9783319942056 010 $a3319942050 024 7 $a10.1007/978-3-319-94205-6 035 $a(CKB)4100000005323110 035 $a(DE-He213)978-3-319-94205-6 035 $a(MiAaPQ)EBC6296149 035 $a(PPN)229502296 035 $a(EXLCZ)994100000005323110 100 $a20180629d2018 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Reasoning $e9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings /$fedited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani 205 $a1st ed. 2018. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2018. 215 $a1 online resource (XVI, 724 p. 128 illus.) 225 1 $aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v10900 311 08$a9783319942049 311 08$a3319942042 327 $aAn 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. 330 $aThis 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. 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v10900 606 $aMachine theory 606 $aArtificial intelligence 606 $aComputer science 606 $aAlgorithms 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aComputer Science Logic and Foundations of Programming 606 $aAlgorithms 606 $aSoftware Engineering 606 $aCompilers and Interpreters 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aComputer science. 615 0$aAlgorithms. 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 14$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aAlgorithms. 615 24$aSoftware Engineering. 615 24$aCompilers and Interpreters. 676 $a004.015113 702 $aGalmiche$b Didier$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSchulz$b Stephan$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSebastiani$b Roberto$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910349422303321 996 $aAutomated Reasoning$9771895 997 $aUNINA