Frontiers of Combining Systems: 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023, Proceedings (Lecture Notes in Artificial Intelligence)

This book constitutes the refereed proceedings of the 14th International Symposium on Frontiers of Combining Systems, FroCoS 2023, held in Prague, Czech Republic, in September 2023. The symposium was co-located with the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023. The 14 papers presented were thorouhgly reviewed and selected from the 22 high-quality paper submissions. They are grouped in the volume according to the following topic classification: analysis of programs and equations; unification; decidable fragments; frameworks; higher-order theorem proving. This is an open access book. Preface Organization Abstracts of Invited Talks Incremental Reasoning in Embedded SAT Solvers On Datatypes, Synergies, and Unicorns: Recent Developments in Theory Combination Contents Analysis of Programs and Equations Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs 1 Introduction 2 Size Bounds by Closed Forms 3 Size and Runtime Bounds for Solvable Loops 3.1 Closed Forms for Solvable Loops 3.2 Periodic Rational Solvable Loops 4 Size Bounds for Integer Programs 5 Completeness of Size and Runtime Analysis for Programs 6 Conclusion and Evaluation References Recurrence-Driven Summations in Automated Deduction 1 Introduction 2 Inference Rule 3 Initialization 4 Propagation 5 Induction 6 Examples 7 Related Work 8 Conclusion References Formal Verification of Bit-Vector Invertibility Conditions in Coq 1 Introduction 2 Preliminaries 2.1 Theory of Bit-Vectors 2.2 Coq 3 Invertibility Conditions and Their Verification 4 The BVList Library 4.1 BVList Without Extensions 4.2 Extending BVList 5 Proving Invertibility Equivalences in Coq 5.1 General Approach 5.2 Detailed Examples 5.3 Results 6 Conclusion and Future Work References Unification Weighted Path Orders Are Semantic Path Orders 1 Introduction 2 Preliminaries 2.1 Term Rewriting 2.2 Weighted Path Orders 3 Semantic Path Orders Based on Order Pairs 4 Simulating WPOs by SPOs 5 Generalized Weighted Path Orders 6 Experimental Results 7 Simulating Dependency Pairs by GWPOs 8 Conclusion References KBO Constraint Solving Revisited 1 Introduction 2 Preliminaries 3 Simple, Right-Ground KBO Constraints 4 Further Constraint Variants and Ordering Relaxation 5 Experiments 6 Discussion References A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems 1 Introduction 2 Preliminaries 3 Level-Commutation of Oriented CTRSs 4 Critical Pair Criteria for Join and Semi-Equational CTRSs 4.1 Level-Confluence of Join and Semi-Equational 3-CTRSs 4.2 Commutation of Semi-Equational 3-CTRSs 5 Conclusion References Decidable Fragments Logic of Communication Interpretation: How to Not Get Lost in Translation 1 Introduction 2 Heterogeneous Distributed Systems 3 Epistemic Logic for Heterogeneous Distributed Systems 4 Soundness and Completeness of EHL 5 Properties of Creed 6 Applications 6.1 Formalizing ``The Murders in the Rue Morgue'' 6.2 Solution to Knights and Knaves 6.3 Modelling of Software Updates 6.4 Comparison to Related Work 7 Conclusion and Future Work References Symbolic Model Construction for Saturated Constrained Horn Clauses 1 Introduction 2 Preliminaries and Notation 2.1 Horn Bernays-Schönfinkel with Linear Arithmetic 2.2 Ordering Literals and Clauses 2.3 Hierarchic Superposition, Redundancy and Saturation 2.4 Interpretations 2.5 Consequence and Least Model 3 Model Construction 4 Conclusion References Frameworks Combining Finite Combination Properties: Finite Models and Busy Beavers 1 Introduction 2 Preliminary Notions 2.1 Many-Sorted Logic 2.2 Theory Combination Properties 3 Relationships Between Model-Theoretic Properties 3.1 General Signatures 3.2 Empty Signatures 4 A Taxonomy of Examples 4.1 The Table 4.2 Theories from ch9BarTolZoh 4.3 New Theories: The Simple Cases 4.4 New Theories: The Busy Beaver 4.5 Theory Operators 5 Conclusion References Formal Reasoning Using Distributed Assertions 1 Introduction 2 Design of DAMF 2.1 Languages, Contexts, and Formulas 2.2 Sequents and Assertions 2.3 Adapters 2.4 Composing Assertions, Trust 2.5 Producing Assertions, Formal Reasoning Tools 2.6 Logical Consistency of Heterogeneous Combinations 3 Implementation: Information, Processes, and Tools 3.1 The Structures of the Global Store 3.2 Processes in DAMF, and Dispatch as an Intermediary Tool 3.3 Edge Systems Example: Abella 4 Discussion: Design Choices and Alternatives 4.1 The Role of Formal Proofs 4.2 Potential Benefits to Mainstream Systems 4.3 Other Use Cases 5 Related Work 6 Conclusion References An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL 1 Introduction 2 Preliminaries 3 Chronological CDCL for CNF-to-d-DNNF Compilation 4 Calculus 5 Proofs 6 Generalization 7 Discussion References Higher-Order Theorem Proving Hammering Floating-Point Arithmetic 1 Introduction 2 Background 2.1 The Sledgehammer Proof Process 2.2 IEEE 754 Binary Floating-Point Arithmetic 3 An Implementation of SMT-LIB Floating-Point Arithmetic in Isabelle/HOL 4 Interpreting Isabelle/HOL Floating-Point Arithmetic in SMT-LIB 4.1 SMT-LIB Logic 4.2 Types 4.3 Constants 5 Evaluation 5.1 Results 5.2 Discussion 6 Related Work 7 Conclusions References Learning Proof Transformations and Its Applications in Interactive Theorem Proving 1 Introduction 1.1 Motivation 1.2 Contributions 2 Proof State Characterizations 2.1 Feature Difference 2.2 Anti-unification 2.3 Tree Difference 2.4 Input Formats 3 Learning Models 4 Experiments 5 Applications 5.1 Tactic Suggestion 5.2 Shortening Proofs 6 Related Work 7 Conclusion References Translating SUMO-K to Higher-Order Set Theory 1 Introduction and Motivation 1.1 Related Work and Contributions 2 The SUMO-K Fragment 2.1 Implicit Type Guards 2.2 Variable Arity Relations and Functions 2.3 Quantification over Relations 2.4 Kappa Binders 2.5 Real Arithmetic 3 Translation of SUMO-K to Set Theory 3.1 High Level Overview: Sets, Terms, Spines and Formulas 3.2 Motivating Examples 3.3 The Translation 4 Interactive Proofs of Translated SUMO Queries 5 ATP Problem Set 6 Future Work 7 Conclusion References Author Index