Automated Deduction - CADE 28 : : 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings.

• Superior document: Lecture Notes in Computer Science Series ; v.12699
• Author: Platzer, André.
• TeilnehmendeR: Sutcliffe, Geoff.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2021.; {copy}2021.
• Year of Publication: 2021
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (655 pages)

Table of Contents

Intro -- 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.