Cover Image

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

Bibliographic Details
Main Author: Pientka, Brigitte.
Other Authors: Tinelli, Cesare.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2023.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of Contents:
  • Intro
  • Preface
  • Organization
  • Invited Talks
  • -Superposition: From Theory to Trophy
  • Nominal Techniques for Software Specification and Verification
  • How Can We Trust AI?
  • Contents
  • Certified Core-Guided MaxSAT Solving
  • 1 Introduction
  • 1.1 Previous Work
  • 1.2 Our Contributions
  • 1.3 Outline of This Paper
  • 2 Preliminaries
  • 3 The OLL Algorithm for Core-Guided MaxSAT Solving
  • 4 Proof Logging for the OLL Algorithm for MaxSAT
  • 5 Experimental Evaluation
  • 6 Concluding Remarks
  • References
  • Superposition with Delayed Unification
  • 1 Introduction
  • 2 Preliminaries
  • 3 Calculus
  • 4 Redundancy Criterion
  • 5 Refutational Completeness
  • 6 Extending to Higher-Order Logic
  • 7 Experimental Results
  • 8 Related Work
  • 9 Conclusion
  • References
  • On Incremental Pre-processing for SMT
  • 1 Introduction
  • 2 Preliminaries
  • 3 Incremental Pre-processing
  • 3.1 Simplification Rules
  • 3.2 Pre-processing Replay
  • 4 Simplification Methods
  • 4.1 Equality Solving
  • 4.2 Unconstrained Sub-terms
  • 4.3 Symbol Elimination and Macros
  • 5 Implementation
  • 6 Related Work
  • 6.1 Pre- and In-processing for SAT and QBF
  • 6.2 Pre-processing for SMT
  • 6.3 Pre-processing for MIP
  • 6.4 Pre-processing in First- and Higher-Order Provers
  • 6.5 Constrained Horn Clauses
  • 7 Summary
  • References
  • Verified Given Clause Procedures
  • 1 Introduction
  • 2 Abstract Given Clause Procedures
  • 3 Otter and iProver Loops
  • 4 DISCOUNT Loop
  • 5 Zipperposition Loop
  • 6 Conclusion
  • References
  • QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
  • 1 Introduction
  • 1.1 High-Level View of the QSMA Algorithm
  • 2 Preliminaries
  • 3 The QSMA Framework
  • 4 The QSMA Algorithm and Its Total Correctness
  • 5 The OptiQSMA Algorithm and Its Total Correctness
  • 6 The YicesQS Solver and Experimental Results.
  • 7 Discussion: Related Work and Future Work
  • References
  • Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
  • 1 Introduction
  • 2 Dynamic Logic of Communicating Hybrid Programs
  • 2.1 Syntax
  • 2.2 Semantics
  • 2.3 Static Semantics
  • 3 Uniform Substitution for CHP
  • 3.1 Semantic Effect of Uniform Substitution
  • 3.2 Uniform Substitution Proof Rule
  • 4 Axiomatic Proof Calculus
  • 5 Related Work
  • 6 Conclusion
  • References
  • An Isabelle/HOL Formalization of the SCL(FOL) Calculus
  • 1 Introduction
  • 2 The SCL(FOL) Calculus
  • 3 Formalization of the SCL(FOL) Calculus
  • 4 Conclusion
  • References
  • SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
  • 1 Introduction
  • 2 Preliminaries
  • 3 SCL Simulates Superposition
  • 4 Conclusion
  • References
  • Formal Reasoning About Influence in Natural Sciences Experiments
  • 1 Introduction
  • 2 Modelling Influence
  • 3 The Calculus of Influence
  • 4 Completeness for Elementary Diamond-Free Schemes
  • 5 Proof Search and Empirical Results
  • 6 Conclusion
  • References
  • A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
  • 1 Introduction
  • 2 A Theory of Cartesian Arrays
  • 2.1 Preliminaries
  • 2.2 Definition of the Theory of Cartesian Arrays
  • 2.3 Complexity of Satisfiability in CaAL
  • 3 Array Semantics of Quantum Circuits
  • 3.1 Quantum Circuits
  • 3.2 Interpretation of Quantum Gates
  • 4 A Decision Procedure for Cartesian Arrays
  • 4.1 Preliminaries
  • 4.2 Proof Rules
  • 4.3 Correctness and Complexity
  • 4.4 Optimizations
  • 5 Preliminary Experimental Result
  • 6 Conclusions
  • References
  • SAT-Based Subsumption Resolution
  • 1 Introduction
  • 2 Illustrative Examples and Main Contributions
  • 3 Preliminaries
  • 4 SAT-Based Subsumption Resolution
  • 5 Subsumption Resolution and SAT Encodings.
  • 5.1 Direct SAT Encoding of Subsumption Resolution
  • 5.2 Indirect SAT Encoding of Subsumption Resolution
  • 5.3 SAT Constraints for Subsumption
  • 6 SAT-Based Subsumption Resolution in Saturation
  • 7 Implementation and Experiments
  • 8 Conclusion
  • References
  • A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
  • 1 Introduction
  • 2 Preliminaries
  • 3 Pragmatic CDCL for Inprocessing
  • 4 Correctness of the Code and Completeness
  • 5 Experience Porting the Development to LLVM
  • 5.1 Required Changes
  • 5.2 Unverified Parts
  • 5.3 Lessons Learned
  • 6 Performance
  • 7 Conclusion
  • References
  • Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
  • 1 Introduction
  • 2 Preliminaries
  • 3 ADCL for Transition Systems
  • 4 Proving Non-Termination with ADCL-NT
  • 5 Related Work and Experiments
  • References
  • COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description)
  • 1 Introduction
  • 2 Satisfiability in the Coalgebraic -Calculus
  • 3 Implementation
  • 4 Evaluation
  • 5 Conclusion
  • References
  • Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
  • 1 Introduction
  • 2 Notation
  • 3 Preliminaries
  • 4 Colouring of Terms and Literals
  • 5 Interpolation for Quantified Formulas
  • 5.1 Interpolation Algorithm
  • 5.2 Full Interpolation Example
  • 6 Combination with Equality-Interpolating Theories
  • 7 Implementation in SMTInterpol
  • 8 Conclusion
  • References
  • Proving Termination of C Programs with Lists
  • 1 Introduction
  • 2 Abstract States for Symbolic Execution
  • 3 Symbolic Execution with List Invariants
  • 3.1 Inferring List Invariants and Generalization of States
  • 3.2 Adapting List Invariants
  • 4 Proving Termination
  • 5 Conclusion, Related Work, and Evaluation
  • References
  • Reasoning About Regular Properties: A Comparative Study
  • 1 Introduction.
  • 2 Preliminaries
  • 3 Existing Algorithms and Tools
  • 3.1 Representation of Automata Transition Relations
  • 3.2 (Non)deterministic Finite Automata
  • 3.3 Alternating Automata
  • 3.4 String Constraints Solvers
  • 3.5 Other Approaches and Tools
  • 4 Benchmarks
  • 5 The Comparison
  • 5.1 Discussion
  • References
  • Program Synthesis in Saturation
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Computable Symbols and Programs
  • 2.2 Saturation and Superposition
  • 2.3 Answer Literals
  • 3 Illustrative Example
  • 4 Program Synthesis with Answer Literals
  • 4.1 From Answer Literals to Programs
  • 4.2 Saturation-Based Program Synthesis
  • 5 Superposition with Answer Literals
  • 6 Computable Unification with Abstraction
  • 7 Implementation and Experiments
  • 8 Related Work
  • 9 Conclusions
  • References
  • A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
  • 1 Introduction
  • 2 Logics
  • 3 Bisequent Calculus for K3 (and LP)
  • 4 Bisequent Calculi for Other Logics
  • 5 Interpolation
  • 6 Conclusion
  • References
  • Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
  • 1 Introduction
  • 2 The DP Framework
  • 3 Probabilistic Term Rewriting
  • 4 Probabilistic Dependency Pairs
  • 4.1 Dependency Tuples and Chains for Probabilistic Term Rewriting
  • 4.2 The Probabilistic DP Framework
  • 5 Conclusion and Evaluation
  • References
  • Verification of NP-Hardness Reduction Functions for Exact Lattice Problems
  • 1 Introduction
  • 1.1 Contributions
  • 1.2 Overview
  • 2 Foundations
  • 2.1 Problem Reductions
  • 2.2 Lattice-Based Computational Problems
  • 2.3 Partition and Subset Sum Problems
  • 2.4 Notation
  • 3 CVP
  • 3.1 Towards the SVP
  • 4 Bounded Homogeneous Linear Equations
  • 4.1 Auxiliary Lemma
  • 4.2 a Partition -3mu b BHLE
  • 4.3 a Partition -3mu b BHLE
  • 5 SVP
  • 6 Other p-Norms.
  • 7 Time Complexity
  • 8 Outlook
  • References
  • Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
  • 1 Introduction
  • 2 Preliminaries
  • 3 Reductions
  • 3.1 Definitional Reduction
  • 3.2 Axiomatic Reduction
  • 3.3 Discussion
  • 4 Evaluation
  • 5 Conclusions
  • References
  • Left-Linear Completion with AC Axioms
  • 1 Introduction
  • 2 Preliminaries
  • 3 Avenhaus' Inference System
  • 3.1 Inference System
  • 3.2 Confluence Criterion
  • 3.3 Correctness Proof
  • 4 Bachmair's Inference System
  • 5 AC Completion
  • 5.1 Limitations of Left-Linear AC Completion
  • 5.2 General AC Completion
  • 6 Implementation
  • 7 Experimental Results
  • 8 Conclusion
  • References
  • On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics EL, EL+
  • 1 Introduction
  • 2 Theories, Convexity, P-Interpolation, Beth Definability
  • 3 Local Theory Extensions
  • 4 R-interpolation in Local Theory Extensions
  • 5 Example: Semilattices with Monotone Operators
  • 6 Applications to EL and EL+-Subsumption
  • 7 Conclusions and Future Work
  • References
  • Theorem Proving in Dependently-Typed Higher-Order Logic
  • 1 Introduction and Related Work
  • 2 Preliminaries: Higher-Order Logic
  • 3 Dependent Function Types
  • 3.1 Language
  • 3.2 Translation
  • 4 Predicate Subtypes
  • 5 Soundness and Completeness
  • 6 Theorem Prover Implementation
  • 7 Conclusion and Future Work
  • References
  • Towards Fast Nominal Anti-unification of Letrec-Expressions
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Data-Structures of Anti-unification Algorithms
  • 3 The Anti-unification Problem for NLLX
  • 3.1 The Algorithm AntiUnifLetr and Its Rules
  • 3.2 From Weak Completeness to Completeness
  • 4 Generalization Algorithm Under Semantic Equalities
  • 4.1 Anti-unification of Garbage-Free Expressions
  • 4.2 Exploiting Semantic Equalities.
  • 5 Conclusion and Future Work.

Similar Items