LEADER 01518nam1 22003013i 450 001 SUN0084963 005 20110801114037.678 100 $a20110801d2000 |0itac50 ba 101 $aita 102 $aIT 105 $a|||| ||||| 200 1 $aˆ1: L'‰impresa sistema vitale$fGaetano M. Golinelli 210 $aPadova$cCEDAM$d2000 215 $aXIX, 354 p.$d24 cm. 463 \1$1001SUN0084962$12001 $a<>approccio sistemico al governo dell'impresa 620 $dPadova$3SUNL000007 700 1$aGolinelli$b, Gaetano M.$3SUNV069007$03341 712 $aCEDAM$3SUNV005537$4650 801 $aIT$bSOL$c20181109$gRICA 912 $aSUN0084963 950 $aUFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI ECONOMIA$d03 PREST IIAb14 $e03 29688 950 $aUFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI ECONOMIA$d03 PREST IIAb14bis $e03 29689 950 $aUFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI ECONOMIA$d03 PREST IIAb14ter $e03 29690 995 $aUFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI ECONOMIA$bIT-CE0106$h29688$kPREST IIAb14$op$qa 995 $aUFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI ECONOMIA$bIT-CE0106$h29689$kPREST IIAb14bis$op$qa 995 $aUFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI ECONOMIA$bIT-CE0106$h29690$kPREST IIAb14ter$op$qa 996 $aImpresa sistema vitale$968473 997 $aUNICAMPANIA LEADER 06451nam 22007215 450 001 996418305603316 005 20200703023833.0 010 $a3-030-51054-9 024 7 $a10.1007/978-3-030-51054-1 035 $a(CKB)4100000011325534 035 $a(MiAaPQ)EBC6283192 035 $a(DE-He213)978-3-030-51054-1 035 $a(PPN)248595342 035 $a(EXLCZ)994100000011325534 100 $a20200629d2020 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Reasoning$b[electronic resource] $e10th International Joint Conference, IJCAR 2020, Paris, France, July 1?4, 2020, Proceedings, Part II /$fedited by Nicolas Peltier, Viorica Sofronie-Stokkermans 205 $a1st ed. 2020. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2020. 215 $a1 online resource (521 pages) 225 1 $aLecture Notes in Artificial Intelligence ;$v12167 311 $a3-030-51053-0 327 $aInteractive Theorem Proving/ HOL -- Competing inheritance paths in dependent type theory: a case study in functional analysis -- A Lean tactic for normalising ring expressions with exponents (short paper) -- Practical proof search for Coq by type inhabitation -- Quotients of Bounded Natural Functors -- Trakhtenbrot?s Theorem in Coq -- Deep Generation of Coq Lemma Names Using Elaborated Terms -- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs -- Validating Mathematical Structures -- Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description) -- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages -- Formalizations -- Formalizing the Face Lattice of Polyhedra -- Algebraically Closed Fields in Isabelle/HOL -- Formalization of Forcing in Isabelle/ZF -- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL -- Formal Proof of the Group Law for Edwards Elliptic Curves -- Verifying Farad_zev-Read type Isomorph-Free Exhaustive Generation -- Verification -- Verified Approximation Algorithms -- Efficient Verified Implementation of Introsort and Pdqsort -- A Fast Verified Liveness Analysis in SSA form -- Verification of Closest Pair of Points Algorithms -- Reasoning Systems and Tools -- A Polymorphic Vampire (short paper) -- N-PAT: A Nested Model-Checker (system description) -- HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description) -- Implementing superposition in iProver (system description) -- Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description) -- Make E Smart Again -- Automatically Proving and Disproving Feasibility Conditions -- µ-term: Verify Termination Properties Automatically (system description) -- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) -- The Imandra Automated Reasoning System (system description) -- A Programmer?s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) -- Sequoia: a playground for logicians (system description) -- Prolog Technology Reinforcement Learning Prover (system description). 330 $aThis 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 ?A Fast Verified Liveness Analysis in SSA Form? is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. 410 0$aLecture Notes in Artificial Intelligence ;$v12167 606 $aMathematical logic 606 $aArtificial intelligence 606 $aComputer logic 606 $aSoftware engineering 606 $aProgramming languages (Electronic computers) 606 $aComputer programming 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 0$aComputer logic. 615 0$aSoftware engineering. 615 0$aProgramming languages (Electronic computers). 615 0$aComputer programming. 615 14$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aProgramming Techniques. 676 $a004.015113 702 $aPeltier$b Nicolas$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSofronie-Stokkermans$b Viorica$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996418305603316 996 $aAutomated Reasoning$9771895 997 $aUNISA