000 04702nam a22006135i 4500
001 978-3-031-38499-8
003 DE-He213
005 20240423125355.0
007 cr nn 008mamaa
008 230902s2023 sz | s |||| 0|eng d
020 _a9783031384998
_9978-3-031-38499-8
024 7 _a10.1007/978-3-031-38499-8
_2doi
050 4 _aQ334-342
050 4 _aTA347.A78
072 7 _aUYQ
_2bicssc
072 7 _aCOM004000
_2bisacsh
072 7 _aUYQ
_2thema
082 0 4 _a006.3
_223
245 1 0 _aAutomated Deduction – CADE 29
_h[electronic resource] :
_b29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings /
_cedited by Brigitte Pientka, Cesare Tinelli.
250 _a1st ed. 2023.
264 1 _aCham :
_bSpringer Nature Switzerland :
_bImprint: Springer,
_c2023.
300 _aXXV, 592 p. 85 illus., 32 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v14132
505 0 _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).
506 0 _aOpen Access
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. .
650 0 _aArtificial intelligence.
650 0 _aMachine theory.
650 0 _aComputer science.
650 0 _aSoftware engineering.
650 1 4 _aArtificial Intelligence.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aSoftware Engineering.
700 1 _aPientka, Brigitte.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aTinelli, Cesare.
_eeditor.
_0(orcid)
_10000-0002-6726-775X
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783031384981
776 0 8 _iPrinted edition:
_z9783031385001
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v14132
856 4 0 _uhttps://doi.org/10.1007/978-3-031-38499-8
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-SOB
942 _cSPRINGER
999 _c177240
_d177240