Automated Deduction - CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings /

This 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. .

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Pientka, Brigitte (Editor), Tinelli, Cesare (Editor)
Format: Electronic eBook
Language:English
Published: Cham : Springer Nature Switzerland : Imprint: Springer, 2023.
Edition:1st ed. 2023.
Series:Lecture Notes in Artificial Intelligence, 14132
Subjects:
Online Access:Link to Metadata
Tags: Add Tag
No Tags, Be the first to tag this record!

MARC

LEADER 00000nam a22000005i 4500
001 978-3-031-38499-8
003 DE-He213
005 20240318083151.0
007 cr nn 008mamaa
008 230902s2023 sz | s |||| 0|eng d
020 |a 9783031384998  |9 978-3-031-38499-8 
024 7 |a 10.1007/978-3-031-38499-8  |2 doi 
050 4 |a Q334-342 
050 4 |a TA347.A78 
072 7 |a UYQ  |2 bicssc 
072 7 |a COM004000  |2 bisacsh 
072 7 |a UYQ  |2 thema 
082 0 4 |a 006.3  |2 23 
245 1 0 |a Automated Deduction - CADE 29  |h [electronic resource] :  |b 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings /  |c edited by Brigitte Pientka, Cesare Tinelli. 
250 |a 1st ed. 2023. 
264 1 |a Cham :  |b Springer Nature Switzerland :  |b Imprint: Springer,  |c 2023. 
300 |a XXV, 592 p. 85 illus., 32 illus. in color.  |b online resource. 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
347 |a text file  |b PDF  |2 rda 
490 1 |a Lecture Notes in Artificial Intelligence,  |x 2945-9141 ;  |v 14132 
505 0 |a Certified 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 |a Open Access 
520 |a This 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 |a Artificial intelligence. 
650 0 |a Machine theory. 
650 0 |a Computer science. 
650 0 |a Software engineering. 
650 1 4 |a Artificial Intelligence. 
650 2 4 |a Formal Languages and Automata Theory. 
650 2 4 |a Computer Science Logic and Foundations of Programming. 
650 2 4 |a Software Engineering. 
700 1 |a Pientka, Brigitte.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Tinelli, Cesare.  |e editor.  |0 (orcid)  |1 0000-0002-6726-775X  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
710 2 |a SpringerLink (Online service) 
773 0 |t Springer Nature eBook 
776 0 8 |i Printed edition:  |z 9783031384981 
776 0 8 |i Printed edition:  |z 9783031385001 
830 0 |a Lecture Notes in Artificial Intelligence,  |x 2945-9141 ;  |v 14132 
856 4 0 |u https://doi.org/10.1007/978-3-031-38499-8  |z Link to Metadata 
912 |a ZDB-2-SCS 
912 |a ZDB-2-SXCS 
912 |a ZDB-2-LNC 
912 |a ZDB-2-SOB 
950 |a Computer Science (SpringerNature-11645) 
950 |a Computer Science (R0) (SpringerNature-43710)