My Account Log in

3 options

Automated Deduction – CADE 29 : 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings / edited by Brigitte Pientka, Cesare Tinelli.

OAPEN Available online

View online

Springer Nature - Springer Nature Link Journals and eBooks - Fully Open Access Available online

View online

SpringerLink Open Access eBooks Available online

View online
Format:
Book
Author/Creator:
Pientka, Brigitte.
Contributor:
Tinelli, C. (Cesare)
Series:
Lecture Notes in Artificial Intelligence, 2945-9141 ; 14132
Language:
English
Subjects (All):
Artificial intelligence.
Machine theory.
Computer science.
Software engineering.
Artificial Intelligence.
Formal Languages and Automata Theory.
Computer Science Logic and Foundations of Programming.
Software Engineering.
Local Subjects:
Artificial Intelligence.
Formal Languages and Automata Theory.
Computer Science Logic and Foundations of Programming.
Software Engineering.
Physical Description:
1 online resource (614 pages)
Edition:
1st ed. 2023.
Place of Publication:
Cham : Springer Nature Switzerland : Imprint: Springer, 2023.
Summary:
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. .
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).
Other Format:
Print version: Pientka, Brigitte Automated Deduction - CADE 29
ISBN:
3-031-38499-7
OCLC:
1396164550

The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.

Find

Home Release notes

My Account

Shelf Request an item Bookmarks Fines and fees Settings

Guides

Using the Find catalog Using Articles+ Using your account