Frontiers of Combining Systems: 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 13th International Symposium on Frontiers of Combining Systems, FroCoS 2021, held in Birmingham, UK, in September 2021. Preface Organization Abstracts of Invited Talk The Strange Career of Interpolation and Definability On the Unreasonable Effectiveness of SAT Solvers General Automation in Coq Through Modular Transformations and SMT Solving Forgetting and Subontology Generation for the Medical Ontology SNOMED CT Contents Calculi and Unification A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic 1 Introduction 2 Preliminaries 3 The Theory of the Hammer 4 Two Supervisor Case Studies 5 Implementation and Experiments 6 Conclusion References Non-disjoint Combined Unification and Closure by Equational Paramodulation 1 Introduction 2 Preliminaries 3 Closure by Equational Paramodulation 4 Equational Syntacticness 5 Hierarchical Unification 6 Combination of Regular Collapse-Free Theories 7 Combination of Theories Closed by E-Paramodulation 8 Conclusion References Symbol Elimination and Applications to Parametric Entailment Problems 1 Introduction 1.1 Motivation 2 Local Extensions; Hierarchical Symbol Elimination 2.1 Locality of Theories of Distances 3 Second-Order Quantifier Elimination 4 Checking Entailment 5 Conclusions References On the Copy Complexity of Width 3 Horn Constraint Systems 1 Introduction 2 Statement of Problems 3 Observations on Copy Complexity 4 Computational Complexity of the CCD Problem 5 Conclusion References Description Logics Restricted Unification in the DL FL0 1 Introduction 2 The DL FL0 and Restrictions 2.1 Syntactically Restricting the Role Depth 2.2 Semantically Restricting the Length of Role Paths 3 Unification in FL0 3.1 Syntactically Restricted Unification in FL0 3.2 Semantically Restricted Unification in FL0 4 Root-to-Frontier Tree Automata 5 Solving Linear Language Equations Using RFAs 5.1 The Syntactically Restricted Case 5.2 The Semantically Restricted Case 6 The Unification Type 6.1 The Semantically Restricted Case 6.2 The Syntactically Restricted Case 7 Conclusion References Combining Event Calculus and Description Logic Reasoning via Logic Programming 1 Introduction 2 Stratified Logic Programs and Model Computation 2.1 Possible Models 2.2 Fusemate Soundness and Completeness 3 Description Logic Interface 3.1 Example 4 Event Calculus Embedding 4.1 Linking Description Logic with the Event Calculus 4.2 Ramification Problem 5 Putting It All Together 6 Conclusions References Semantic Forgetting in Expressive Description Logics 1 Introduction 2 Getting Started 3 Forgetting Method 4 Eliminating Helper Symbols 5 Discussion of the Forgetting Method 6 Preserving Ontology Structure 7 Empirical Evaluation 8 Conclusions References Interactive Theorem Proving Improving Automation for Higher-Order Proof Steps 1 Introduction 2 The Difficulty of Second-Order Proofs in TLA+ 3 The Encoding of TLA+ into THF 3.1 Overview 3.2 Recovering Formulas 3.3 Arithmetic 3.4 Set Extensionality 4 Evaluation 4.1 Proof Simplification 4.2 Results 4.3 Discussion 5 Conclusion References JEFL: Joint Embedding of Formal Proof Libraries 1 Introduction 2 Previous Works and the tt Format 3 The Architecture of JEFL 3.1 Similarity Through Embedding 3.2 Adaptation of the tt Format in Word2Vec 3.3 The SGD Updates of Word2Vec 3.4 The fasttext Implementation of Word2Vec 4 Experimenting with JEFL 5 Comparison with Iterative Pattern-Matching 5.1 Advantages and Drawbacks of Iterative Pattern Matching 6 Conclusion 6.1 Limitations and Future Work References Machine Learning Fast and Slow Enigmas and Parental Guidance 1 Introduction: The Fast and The Smart 1.1 Contributions 2 Saturation Proving and Its Guidance by ENIGMA 3 Cooperative Filtering: Faster and Smarter 3.1 Fast GNN Evaluation Using a GPU Server 3.2 Best of Both Worlds: GNN with GBDT Filtering 3.3 Parental Guidance: Pruning the Given Clause Loop 4 Experimental Setting and Baselines 4.1 Evaluation Problems and Training Data 4.2 Baseline ENIGMA Models 4.3 Training of the Parental GBDT Models 5 Evaluation of the New Methods 5.1 Speedup by Using a GPU Server 5.2 Evaluation of 2-Phase ENIGMA 5.3 Evaluation of the Parental Guidance Combined with Dlarge 5.4 Parental Guidance with Glarge and 3-Phase ENIGMAs 6 Conclusion and Examples References Vampire with a Brain Is a Good ITP Hammer 1 Introduction 2 Internal Guidance of an ATP Using Machine Learning 3 Neural Classification of Clause Derivations 3.1 A Recursive Neural Network Clause Derivation Classifier 3.2 Information Sources, the Conjecture, and SInE Levels 3.3 Training the Network 3.4 Implementation and the Parallel Training Setup 4 Experiments 4.1 Data Preparation 4.2 Training 4.3 Evaluation with the Prover 4.4 Information Source Performance Breakdown 4.5 Looping to Get Even Better 5 Conclusion References Satisfiability Modulo Theories Optimization Modulo Non-linear Arithmetic via Incremental Linearization 1 Introduction 2 Background 2.1 Optimization Modulo Theories 2.2 SMT(NIRA) via Incremental Linearization 3 Optimization Modulo Non-linear Arithmetic 3.1 Linear Optimization Search 3.2 Algorithm Improvements 4 Experimental Evaluation 5 Conclusions and Future Work References Quantifier Simplification by Unificationpg in SMT 1 Introduction 2 CDCL(T) and Quantifier Instantiation 2.1 Preliminaries 2.2 Preprocessing 2.3 Instantiation Techniques 3 Quantifier Simplification by Unification 3.1 The Core Rule 3.2 The Simplification Within the SMT Solver 3.3 Variants 4 Implementation 4.1 Indexing and Unification Without Skolemization 5 Evaluation 5.1 Baseline Comparison 5.2 Strategy Scheduling 6 Conclusion References Verification Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems 1 Introduction 1.1 Implementation 2 Preliminaries 2.1 Terms and Substitutions 2.2 Equational Theories 3 Modes of Operation 4 The Invertibility Problem 4.1 Implementation 5 Decision Problems for Symbolic Security 5.1 Undecidable Decision Problems for Block Ciphers 5.2 An Algorithm for Checking Symbolic Security 5.3 Implementation 6 Conclusions References Formal Analysis of Symbolic Authenticity 1 Introduction 2 Preliminaries 3 Formal Analysis of Symbolic Authenticity of Fixed-Length AE Schemes 3.1 Modelling Fixed-Length AE Schemes 3.2 Symbolic Authenticity for Fixed-Length AE Schemes 3.3 Inference system 4 Formal Analysis of Symbolic Authenticity of General AE Schemes 4.1 Modelling General AE Schemes 4.2 Symbolic Authenticity for General AE Schemes 4.3 Inference System 5 Conclusions and Future Work References Formal Verification of a Java Component Using the RESOLVE Framework 1 Introduction 2 Background 2.1 Previous Work 2.2 Existing BDD Implementations 2.3 Applications of BDDs 2.4 Object-Oriented and Automatic Verification 3 Combining Value and Reference Semantics 3.1 RESOLVE and Value-Based Semantics 3.2 RESOLVE with Object-Oriented Languages 4 Formal Verification of the BDD Component 4.1 Loop Invariants and Iteration 4.2 Reasoning Tables and Proofs 5 Limitation in the Component Design Pattern 6 Corrections to the Component 7 Conclusion References Author Index