001480676 000__ 05056cam\\22006257i\4500
001480676 001__ 1480676
001480676 003__ OCoLC
001480676 005__ 20231031003304.0
001480676 006__ m\\\\\o\\d\\\\\\\\
001480676 007__ cr\un\nnnunnun
001480676 008__ 230905s2023\\\\sz\a\\\\o\\\\\101\0\eng\d
001480676 020__ $$a9783031384998$$q(electronic bk.)
001480676 020__ $$a3031384997$$q(electronic bk.)
001480676 020__ $$z9783031384981
001480676 0247_ $$a10.1007/978-3-031-38499-8$$2doi
001480676 035__ $$aSP(OCoLC)1396164550
001480676 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dEBLCP$$dOCLCO$$dWSU
001480676 049__ $$aISEA
001480676 050_4 $$aQA76.9.A96$$bI58 2023eb
001480676 08204 $$a511.3/6028563$$223/eng/20230905
001480676 1112_ $$aInternational Conference on Automated Deduction$$n(29th :$$d2023 :$$cRome, Italy)
001480676 24510 $$aAutomated deduction -- CADE 29 :$$b29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings /$$cBrigitte Pientka, Cesare Tinelli, editors.
001480676 2463_ $$aCADE 29
001480676 264_1 $$aCham, Switzerland :$$bSpringer,$$c2023.
001480676 300__ $$a1 online resource (xxv, 592 pages) :$$billustrations (some color).
001480676 336__ $$atext$$btxt$$2rdacontent
001480676 337__ $$acomputer$$bc$$2rdamedia
001480676 338__ $$aonline resource$$bcr$$2rdacarrier
001480676 4901_ $$aLecture notes in artificial intelligence
001480676 4901_ $$aLecture notes in computer science ;$$v14132
001480676 4901_ $$aLNCS sublibrary, SL 7, Artificial intelligence
001480676 500__ $$aIncludes author index.
001480676 5050_ $$aCertified Core-Guided MaxSAT Solving -- Superposition with Delayed Unification -- On Incremental Pre-processing for SMT -- Verified Given Clause Procedures -- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment -- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs -- An Isabelle/HOL Formalization of the SCL(FOL) Calculus -- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning -- Formal Reasoning about Influence in Natural Sciences Experiments -- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification) -- SAT-Based Subsumption Resolution -- A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper) -- Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper) -- COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description) -- Choose your Colour: Tree Interpolation for Quantified Formulas in SMT -- Proving Termination of C Programs with Lists -- Reasoning about Regular Properties: A Comparative Study -- Program Synthesis in Saturation -- A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus -- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs -- Verification of NP-hardness Reduction Functions for Exact Lattice Problems -- Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic -- Left-Linear Completion with AC Axioms -- On P -interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+ -- Theorem Proving in Dependently-Typed Higher-Order Logic -- Towards Fast Nominal Anti-Unification of Letrec-Expressions -- Confluence Criteria for Logically Constrained Rewrite Systems -- Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory -- An Experimental Pipeline for Automated Reasoning in Natural Language (Short paper) -- Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness -- Decidability of difference logic over the reals with uninterpreted unary predicates -- Incremental Rewriting Modulo SMT -- Iscalc: an Interactive Symbolic Computation Framework (System Description).
001480676 5060_ $$aOpen access.$$5GW5XE
001480676 520__ $$aThis open access book constitutes the proceedings of the 29th International Conference on Automated Deduction, CADE 29, which took place in Rome, Italy, during July 2023.
001480676 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed September 5, 2023).
001480676 650_6 $$aThéorèmes$$xDémonstration automatique$$vCongrès.
001480676 650_6 $$aLogique symbolique et mathématique$$vCongrès.
001480676 650_0 $$aAutomatic theorem proving$$vCongresses.
001480676 650_0 $$aLogic, Symbolic and mathematical$$vCongresses.$$vCongresses$$0(DLC)sh2008107112
001480676 655_0 $$aElectronic books.
001480676 655_7 $$aConference papers and proceedings.$$2lcgft
001480676 7001_ $$aPientka, Brigitte,$$eeditor.$$1https://orcid.org/0000-0002-2549-4276
001480676 7001_ $$aTinelli, C.$$q(Cesare),$$eeditor.$$1https://orcid.org/0000-0002-6726-775X
001480676 830_0 $$aLecture notes in computer science.$$pLecture notes in artificial intelligence.
001480676 830_0 $$aLecture notes in computer science ;$$v14132.
001480676 830_0 $$aLNCS sublibrary.$$nSL 7,$$pArtificial intelligence.
001480676 852__ $$bebk
001480676 85640 $$3Springer Nature$$uhttps://link.springer.com/10.1007/978-3-031-38499-8$$zOnline Access$$91397441.2
001480676 909CO $$ooai:library.usi.edu:1480676$$pGLOBAL_SET
001480676 980__ $$aBIB
001480676 980__ $$aEBOOK
001480676 982__ $$aEbook
001480676 983__ $$aOnline
001480676 994__ $$a92$$bISE