Cover Image

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

Bibliographic Details
Main Author: Platzer, André.
Other Authors: Sutcliffe, Geoff.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2021.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
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.

Similar Items