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

• Superior document: Lecture Notes in Computer Science Series ; v.14132
• Author: Pientka, Brigitte.
• TeilnehmendeR: Tinelli, Cesare.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2023.; ©2023.
• Year of Publication: 2023
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (614 pages)

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.