LEADER 06189nam 22007215 450 001 9910409661703321 005 20200701042719.0 010 $a3-030-51074-3 024 7 $a10.1007/978-3-030-51074-9 035 $a(CKB)4100000011325535 035 $a(MiAaPQ)EBC6295399 035 $a(DE-He213)978-3-030-51074-9 035 $a(PPN)248595350 035 $a(EXLCZ)994100000011325535 100 $a20200629d2020 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Reasoning $e10th International Joint Conference, IJCAR 2020, Paris, France, July 1?4, 2020, Proceedings, Part I /$fedited by Nicolas Peltier, Viorica Sofronie-Stokkermans 205 $a1st ed. 2020. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2020. 215 $a1 online resource (553 pages) 225 1 $aLecture Notes in Artificial Intelligence ;$v12166 311 $a3-030-51073-5 327 $aInvited Paper -- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints -- SAT; SMT and QBF -- An SMT Theory of Fixed-Point Arithmetic -- Covered Clauses Are Not Propagation Redundant -- The Resolution of Keller?s Conjecture -- How QBF Expansion Makes Strategy Extraction Hard -- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates -- Solving bit-vectors with MCSAT: explanations from bits and pieces -- Monadic Decomposition in Integer Linear Arithmetic -- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis -- Decision Procedures and Combination of Theories -- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols -- Combined Covers and Beth Definability -- Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates -- A Decision Procedure for String to Code Point Conversion -- Politeness for The Theory of Algebraic Datatypes -- Superposition -- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations -- A Combinator-Based Superposition Calculus for Higher-Order Logic -- Subsumption Demodulation in First-Order Theorem Proving -- A Comprehensive Framework for Saturation Theorem Proving -- Proof Procedures -- Possible Models Computation and Revision - A Practical Approach -- SGGS Decision Procedures -- Integrating Induction and Coinduction via Closure Operators and Proof Cycles -- Logic-Independent Proof Search in Logical Frameworks (short paper) -- Layered Clause Selection for Theory Reasoning (short paper) -- Non Classical Logics -- Description Logics with Concrete Domains and General Concept Inclusions Revisited -- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic -- Constructive Hybrid Games -- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) -- NP Reasoning in the Monotone µ-Calculus -- Soft subexponentials and multiplexing -- Mechanised Modal Model Theory. 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 ?Constructive Hybrid Games? is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. 410 0$aLecture Notes in Artificial Intelligence ;$v12166 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 $a006.3 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 $a9910409661703321 996 $aAutomated Reasoning$9771895 997 $aUNINA