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