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

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

Show other versions (2)

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:
Artificial intelligence.
Machine theory.
Computer science.
Software engineering.
Artificial Intelligence.
Formal Languages and Automata Theory.
Computer Science Logic and Foundations of Programming.
Software Engineering.
Online Access:Link to Metadata
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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).

Similar Items