000938127 000__ 05941cam\a2200577Ia\4500
000938127 001__ 938127
000938127 005__ 20230306151745.0
000938127 006__ m\\\\\o\\d\\\\\\\\
000938127 007__ cr\un\nnnunnun
000938127 008__ 200725s2020\\\\sz\\\\\\ob\\\\101\0\eng\d
000938127 019__ $$a1178998544$$a1182451491$$a1182922837$$a1183928418
000938127 020__ $$a9783030510749$$q(electronic book)
000938127 020__ $$a3030510743$$q(electronic book)
000938127 020__ $$z9783030510732
000938127 0247_ $$a10.1007/978-3-030-51
000938127 035__ $$aSP(OCoLC)on1163475084
000938127 035__ $$aSP(OCoLC)1163475084$$z(OCoLC)1178998544$$z(OCoLC)1182451491$$z(OCoLC)1182922837$$z(OCoLC)1183928418
000938127 040__ $$aEBLCP$$beng$$cEBLCP$$dGW5XE$$dEBLCP$$dLQU$$dOCLCF
000938127 049__ $$aISEA
000938127 050_4 $$aQA76.9.A96
000938127 08204 $$a511.3/6028563$$223
000938127 1112_ $$aIJCAR (Conference)$$n(10th :$$d2020 :$$cOnline)
000938127 24510 $$aAutomated reasoning :$$b10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings.$$nPart I /$$cNicolas Peltier, Viorica Sofronie-Stokkermans (eds.).
000938127 2463_ $$aIJCAR 2020
000938127 260__ $$aCham :$$bSpringer,$$c2020.
000938127 300__ $$a1 online resource (553 pages).
000938127 336__ $$atext$$btxt$$2rdacontent
000938127 337__ $$acomputer$$bc$$2rdamedia
000938127 338__ $$aonline resource$$bcr$$2rdacarrier
000938127 4901_ $$aLecture notes in computer science ;$$v12166
000938127 4901_ $$aLecture notes in artificial intelligence
000938127 4901_ $$aLNCS Sublibrary: SL 7, Artificial Intelligence
000938127 500__ $$aInternational conference proceedings.
000938127 500__ $$a"These volumes contain the papers presented at the 10th International Joint Conference on Automated Reasoning (IJCAR 2020) initially planned to be held in Paris, but -- due to the COVID-19 pandemic -- held by remote conferencing during July 1-4, 2020."
000938127 504__ $$aIncludes bibliographical references and author index.
000938127 5050_ $$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 Kellers 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.
000938127 506__ $$aAccess limited to authorized users.
000938127 520__ $$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.
000938127 588__ $$aDescription based on print version record.
000938127 650_0 $$aAutomatic theorem proving$$vCongresses.
000938127 650_0 $$aComputer logic$$vCongresses.
000938127 7001_ $$aPeltier, Nicolas.
000938127 7001_ $$aSofronie-Stokkermans, Viorica.
000938127 77608 $$iPrint version:$$aPeltier, Nicolas$$tAutomated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I$$dCham : Springer International Publishing AG,c2020$$z9783030510732
000938127 830_0 $$aLecture notes in computer science ;$$v12166.
000938127 830_0 $$aLecture notes in computer science.$$pLecture notes in artificial intelligence.
000938127 830_0 $$aLNCS sublibrary.$$nSL 7,$$pArtificial intelligence.
000938127 852__ $$bebk
000938127 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-030-51074-9$$zOnline Access$$91397441.1
000938127 909CO $$ooai:library.usi.edu:938127$$pGLOBAL_SET
000938127 980__ $$aEBOOK
000938127 980__ $$aBIB
000938127 982__ $$aEbook
000938127 983__ $$aOnline
000938127 994__ $$a92$$bISE