Automated Deduction - CADE 29 : : 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.14132 |
---|---|
: | |
TeilnehmendeR: | |
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
|
Online Access: | |
Physical Description: | 1 online resource (614 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
LEADER | 11158nam a22004693i 4500 | ||
---|---|---|---|
001 | 50030733646 | ||
003 | MiAaPQ | ||
005 | 20240229073851.0 | ||
006 | m o d | | ||
007 | cr cnu|||||||| | ||
008 | 240229s2023 xx o ||||0 eng d | ||
020 | |a 9783031384998 |q (electronic bk.) | ||
020 | |z 9783031384981 | ||
035 | |a (MiAaPQ)50030733646 | ||
035 | |a (Au-PeEL)EBL30733646 | ||
035 | |a (OCoLC)1396164550 | ||
040 | |a MiAaPQ |b eng |e rda |e pn |c MiAaPQ |d MiAaPQ | ||
050 | 4 | |a Q334-342 | |
100 | 1 | |a Pientka, Brigitte. | |
245 | 1 | 0 | |a Automated Deduction - CADE 29 : |b 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings. |
250 | |a 1st ed. | ||
264 | 1 | |a Cham : |b Springer International Publishing AG, |c 2023. | |
264 | 4 | |c ©2023. | |
300 | |a 1 online resource (614 pages) | ||
336 | |a text |b txt |2 rdacontent | ||
337 | |a computer |b c |2 rdamedia | ||
338 | |a online resource |b cr |2 rdacarrier | ||
490 | 1 | |a Lecture Notes in Computer Science Series ; |v v.14132 | |
505 | 0 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 5 Conclusion and Future Work. | |
588 | |a Description based on publisher supplied metadata and other sources. | ||
590 | |a Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. | ||
655 | 4 | |a Electronic books. | |
700 | 1 | |a Tinelli, Cesare. | |
776 | 0 | 8 | |i Print version: |a Pientka, Brigitte |t Automated Deduction - CADE 29 |d Cham : Springer International Publishing AG,c2023 |z 9783031384981 |
797 | 2 | |a ProQuest (Firm) | |
830 | 0 | |a Lecture Notes in Computer Science Series | |
856 | 4 | 0 | |u https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=30733646 |z Click to View |