Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings (Lecture Notes in Computer Science Book 12699)

This open access book constitutes the proceeding of the 28th International Conference on Automated Deduction, CADE 28, held virtually in July 2021. The 29 full papers and 7 system descriptions presented together with 2 invited papers were carefully reviewed and selected from 76 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. The papers are organized in the following topics: Logical foundations; theory and principles; implementation and application; ATP and AI; and system descriptions. Preface Organization Contents Invited Talks Non-well-founded Deduction for Induction and Coinduction 1 Introduction 2 The Principles of Induction and Coinduction 2.1 Algebraic Formalization of Induction and Coinduction 2.2 Transitive (Co)closure Operators 3 Non-well-founded Deduction for Induction 3.1 Non-well-founded Proof Theory 3.2 Explicit vs. Implicit Induction in Transitive Closure Logic 4 Adding Coinductive Reasoning 4.1 Implicit Coinduction in Transitive (Co)closure Logic 4.2 Applications in Automated Proof Search 4.2.1 Program Equivalence in the TcC Framework 5 Perspectives and Open Questions 5.1 Implementing Non-well-founded Machinery 5.2 Relative Power of Explicit and Implicit Reasoning References Towards the Automatic Mathematician 1 Introduction 2 Towards the Automatic Mathematician 2.1 Neural Network Architectures 2.2 Training Methodology 2.3 Instant Utilization of New Premises 2.4 Natural Language 3 Conclusion References Logical Foundations Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity 1 Introduction 2 SCI 3 Tableaux 3.1 Tableau System for SCI 3.2 Soundness and Completeness4 3.3 Termination 3.4 Limiting the Number of Labels 4 Implementation 4.1 Overview 4.2 Technical Notes 4.3 Test Results 5 Conclusions References Learning from Łukasiewicz and Meredith: Investigations into Proof Structures 1 Introduction 2 Relating Formal Human Proofs with ATP Proofs 3 Condensed Detachment and a Formal Basis 3.1 Proof Structures: D-Terms, Tree Size and Compacted Size 3.2 Proof Structures, Formula Substitutions and Semantics 4 Reducing the Proof Size by Replacing Subproofs 5 Properties of Meredith’s Refined Proof 6 First Experiments 7 Conclusion References Efficient Local Reductions to Basic Modal Logic 1 Introduction 2 Preliminaries 3 Layered Normal Form with Sets of Levels 4 Correctness 5 Comparison With Related Work 6 Evaluation 7 Conclusion and Future Work References Isabelle's Metalogic: Formalization and Proof Checker 1 Introduction 2 Related Work 3 Preliminaries 4 Types and Terms 5 Classes and Sorts 6 Signatures 7 Logic 7.1 Basic Inference Rules 7.2 Equality 7.3 Type Class Reasoning 8 Proof Terms and Checker 9 Size and Structure of the Formalization 10 Integration with Isabelle 11 Running the Proof Checker 12 Trust Assumptions 13 Future Work A Appendix References Theory and Principles The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints 1 Introduction 2 Preliminaries 3 The ksmt Calculus 3.1 Sufficient Termination Conditions 4 δ-decidability 5 δ-ksmt 5.1 Soundness 5.2 δ-completeness 6 Local ε-full Linearisations 7 Conclusion References Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning 1 Introduction 2 Preliminaries 3 Modeling Parametric Systems as Array-based Transition Systems 3.1 Universal invariant problem for array-based systems 4 Overview of the Method 5 Modified Parameter Abstraction 5.1 Abstraction Computation 5.2 Stuttering Simulation 6 Refinement 6.1 From Invariants to Universal Lemmas 7 Related Work 8 Experimental Evaluation 9 Conclusions References Politeness and Stable Infiniteness: Stronger Together 1 Introduction 2 Preliminaries 2.1 Signatures and Structures 2.2 Polite Theories 3 Politeness and Strong Politeness 3.1 Witnesses vs. Strong Witnesses 3.2 A Polite Theory that is not Strongly Polite 3.3 The Case of Mono-sorted Polite Theories 3.4 Mono-sorted Finite Witnessability 4 A Blend of Polite and Stably-Infinite Theories 4.1 Refined Combination Theorem 4.2 Proof of Theorem 4 5 Preliminary Case Study 6 Conclusion References Equational Theorem Proving Modulo 1 Introduction 2 Preliminaries 3 Constrained Clauses 4 Inference Rules 5 Redundancy Criteria and Contraction Techniques 6 Refutational Completeness 7 Conclusion References Unifying Decidable Entailments in Separation Logic with Inductive Definitions 1 Introduction 2 Definitions 3 Decidable Entailment Problems 4 Reducing Safe to Established Entailments 4.1 Expansions and Truncations 4.2 Transforming the Consequent 4.3 Transforming the Antecedent 4.4 Transforming Entailments 5 Conclusion and Future Work References Subformula Linking for Intuitionistic Logic with Application to Type Theory 1 Introduction 2 Subformula Linking for Intuitionistic First-Order Logic 2.1 The Propositional Fragment 2.2 Quantifiers 3 Incorporating Arity-Typed λ-Terms 4 Application: Embedding Intuitionistic Type Theories 5 Conclusion and Future Directions References Efficient SAT-based Proof Search in Intuitionistic Propositional Logic 1 Introduction 2 Preliminary Notions 3 The Calculus C→ 4 The Procedure proveR 5 Related Work and Experimental Results References Proof Search and Certificates for Evidential Transactions 1 Introduction 2 Cyberlogic Proof Theory 3 Cyberlogic Programs 3.1 Cyberlogic Program Syntax 3.2 CPS Proof Search 4 Proof Certificates 5 Related Work 6 Conclusions References Non-clausal Redundancy Properties 1 Introduction 2 Preliminaries 3 Redundancy for Boolean Functions 4 BDD Redundancy Properties 5 Gaussian Elimination 6 Results 7 Conclusion References Multi-Dimensional Interpretations for Termination of Term Rewriting 1 Introduction 2 Preliminaries 3 Notes on Reduction Pairs 4 Interpretation Methods as Derivers 5 Multi-Dimensional Interpretations 6 Arctic Interpretations 7 Strict Monotonicity 8 Implementation and Experiments 9 Conclusion References Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures 1 Introduction 2 Preliminaries 2.1 Proofs 2.2 Derivers 3 Measuring Proofs 3.1 Monotone Recursive Measures 4 Complexity Results 4.1 The General Case 4.2 Proof Depth 4.3 The Tree Size Measure 5 Conclusion References Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes 1 Introduction 2 Preliminaries 3 A Tale of Two Entailments 3.1 Classical Entailment and CQ-Entailment 3.2 IQ-Entailment 4 Canonical Repairs 5 Optimized Repairs 6 Evaluation 7 Conclusion References Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance 1 Introduction 2 Resolution Proof Transformation 3 A Generalized Completeness Proof for SOS 4 A new Notion of Relevance 5 Conclusion References A Unifying Splitting Framework 1 Introduction 2 Preliminaries 3 Splitting Calculi 4 Model-Guided Provers 5 Locking Provers 6 AVATAR-Based Provers 7 Application to Other Architectures 8 Conclusion Integer Induction in Saturation 1 Introduction 2 Motivating Examples 2.1 Preliminaries 2.2 Examples 3 Integer Induction 4 Integer Induction in Saturation-Based Proof Search 5 Implementation and Experiments 5.1 Implementation 5.2 Benchmarks 5.3 Experimental Setup 5.4 Experimental Results 6 Related Work 7 Conclusions References Superposition with First-class Booleans and Inprocessing Clausification 1 Introduction 2 Logic 3 The Calculus 4 Refutational Completeness 5 Inprocessing Clausification Methods 6 Implementation 7 Evaluation 8 Related Work and Conclusion Acknowledgment References Superposition for Full Higher-order Logic 1 Introduction 2 Logic 3 The Calculus 4 Refutational Completeness 5 Implementation 6 Evaluation 7 Conclusion Acknowledgment References Implementation and Application Making Higher-Order Superposition Work 1 Introduction 2 Background and Setting 3 Preprocessing Higher-Order Problems 4 Reasoning about Formulas 5 Enumerating Infinitely Branching Inferences 6 Controlling Prolific Rules 7 Controlling the Use of Backends 8 Comparison with Other Provers 9 Discussion and Conclusion References Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver 1 Introduction 2 Background Preliminaries 3 Logical Foundations 3.1 Inference Rules 3.2 Integrating Proof Generation into BDD Operations 4 Integrating Proof Generation into a QBF Solver 4.1 Dual Proof Generation 4.2 Clause Removal 4.3 Specializing to Refutation or Satisfaction Proofs 5 Experimental Results 6 Conclusions Acknowledgements. References Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant 1 Introduction 2 veriT and Proofs 3 Overview of the veriT-Powered smt Tactic 4 Tuning the Reconstruction 4.1 Preprocessing Rules 4.2 Implicit Steps 4.3 Arithmetic Reasoning 4.4 Selective Decoding of the First-order Encoding 4.5 Skipping Steps 5 Evaluation 5.1 Strategies 5.2 Improvements of Sledgehammer Results 5.3 Speed of Reconstruction 6 Related Work 7 Conclusion References An Automated Approach to the Collatz Conjecture 1 Introduction 2 Preliminaries 2.1 String Rewriting Systems 2.2 Interpretation Method 2.3 Generalized Collatz Functions 3 Rewriting the Collatz Function 3.1 Rewriting in Unary 3.2 Rewriting in Mixed Base 4 Automated Proofs 4.1 Convergence of W 4.2 Farkas’ Variant 4.3 Subsets of T 4.4 Odd Trajectories 4.5 Collatz Trajectories Modulo 8 5 More Problems to Approach via Rewriting 6 Related Work 7 Future Work References Verified Interactive Computation of Definite Integrals 1 Introduction 2 Overall Architecture 3 Integration Rules 3.1 Simplification 3.2 Trigonometric Identities 3.3 Substitution 3.4 Integration by Parts 3.5 Rewriting 3.6 Splitting an Integral 3.7 Solving Equations 4 User Interface 4.1 Substitution 4.2 Rational Functions 4.3 Trigonometric Identities 4.4 Slagle's Method 5 Proof Translation 5.1 Introduction to HolPy 5.2 Background Library 5.3 Structure of Proof Automation 5.4 Inequality Checking 5.5 Simplification 5.6 Applying Theorems 6 Evaluation and Examples 7 Conclusion References ATP and AI Confidences for Commonsense Reasoning 1 Introduction 2 Interpretation and Encoding of Uncertainty 2.1 Sources, Representation and Meaning of Statements, Confidences and Dependencies 3 The CONFER Extension Framework for CSR 3.1 Resolution Method 3.2 Queries and Answers 3.3 Top Level of the Algorithm 3.4 C-Resolution 3.5 Cumulative Con dence 3.6 Negative Evidence 4 Implementation and Experimental Results 4.1 Comparing Con dences 4.2 Performance 5 Summary and Future Work References Neural Precedence Recommender 1 Introduction 2 Preliminaries 2.1 Saturation-Based Theorem Proving 2.2 Superposition Calculus 2.3 Neural Networks 3 Architecture 3.1 Graph Constructor: From CNF to Graphs 3.2 GCN: From Graphs to Symbol Embeddings 3.3 Output Layer: From Symbol Embeddings to Symbol Costs 3.4 Sort: From Symbol Costs to Precedence 4 Training Procedure 4.1 Precedence Cost 4.2 Learning to Rank Precedences 5 Experimental Evaluation 5.1 Environment 5.2 Dataset Preparation 5.3 Hyperparameters 5.4 Training Procedure 5.5 Final Evaluation 5.6 Results 6 Related Work 7 Conclusion and Future Work Acknowledgments References Improving ENIGMA-style Clause Selection while Learning From History 1 Introduction 2 ATPs, Clause Selection, and Machine Learning 2.1 Traditional Approaches to Clause Selection 2.2 ENIGMA-style Machine-Learned Clause Selection Guidance 2.3 Integrating the Learned Advice 3 Layered Clause Selection and Lazy Model Evaluation 3.1 Lazy Model Evaluation 4 A Neural Classification of Clause Derivations 4.1 Recursive Neural Networks 4.2 Architecture Details 4.3 Training the Network 4.4 An Abstraction for Compression and Caching 5 Experiments 5.1 Data Preparation 5.2 Training 5.3 Advice Integration 5.4 Evaluation Speed, Lazy Evaluation, and Abstraction Caching 5.5 Positive Bias 5.6 Learning from Guided Proofs and Negative Mining 6 Conclusion Acknowledgement References System Descriptions A Normative Supervisor for Reinforcement Learning Agents 1 Introduction 2 Background 3 The Normative Supervisor 3.1 Configuring the Norm Base 3.2 Automating Translation 3.3 Classify and Assess Conclusions 3.4 Revising the Norm Base 4 Evaluation and Conclusion References Automatically Building Diagrams for Olympiad Geometry Problems 1 Introduction 2 Background 2.1 Olympiad-Level Geometry Problem Statements 2.2 Challenge: Globally Coupled Constraints 2.3 Challenge: Root Resolution 3 Methods 3.1 GMBL: Overview 3.2 GMBL: Commands 3.3 GMBL: Functions and Predicates 3.4 Auxiliary Losses 3.5 Implementation 4 Results 5 Future Work 6 Related Work 7 Conclusion References The Fusemate Logic Programming System 1 Introduction 2 Fusemate Programs 3 Model Computation 4 Shallow Embedding in Scala 5 Embedding Description Logic ALCIF 6 Conclusions References Twee: An Equational Theorem Prover 1 Introduction 2 Architecture 3 Redundancy Criteria 3.1 Ground Joinability Testing 3.2 Connectedness 4 Implementation 4.1 Terms 4.2 Indexing 4.3 The Passive Set 5 Evaluation 6 Future Work 7 Conclusion References The Isabelle/Naproche Natural Language Proof Assistant 1 Introduction 2 Natural Proof Assistants 3 Isabelle/Naproche 4 Formalizing in ForTheL 4.1 Example 4.2 The ForTheL Language 5 Architecture of the Naproche System 5.1 Tokenizing and Parsing 5.2 LATEX Processing 5.3 Logical Processing 5.4 Ontological Checking by the •aproche Reasoner 5.5 Logical Checking by the •aproche Reasoner 5.6 Communication with an External ATP 6 Integration into Isabelle 7 Related and Future Work References The Lean 4 Theorem Prover and Programming Language 1 Introduction 2 Lean by Example 3 The Code Generator 4 The User Interface 5 Conclusion References Harpoon: Mechanizing Metatheory Interactively 1 Introduction 2 Proof Development in Harpoon 2.1 Initial setup: encoding the language 2.2 Termination Property: intros, split, unbox, and solve 2.3 Setup continued: reducibility 2.4 Backwards Closed Property: msplit, suffices, and by 3 Implementation of Harpoon 4 Empirical evaluation of Harpoon 5 Related work 6 Conclusion References Author Index