Automated Deduction – CADE 28 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings /
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...
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Language: | English |
| Published: |
Cham :
Springer International Publishing : Imprint: Springer,
2021.
|
| Edition: | 1st ed. 2021. |
| Series: | Lecture Notes in Artificial Intelligence ;
12699 |
| Subjects: | |
| Online Access: | https://doi.org/10.1007/978-3-030-79876-5 |
Table of Contents:
- Invited Talks
- Non-well-founded Deduction for Induction and Coinduction
- Towards the Automatic Mathematician
- Logical Foundations
- Tableau-based decision procedure for non-Fregean logic of sentential identity
- Learning from Lukasiewicz and Meredith: Investigations into Proof Structures
- Efficient Local Reductions to Basic Modal Logic
- Isabelle's Metalogic: Formalization and Proof Checker
- Theory and Principles
- The ksmt calculus is a delta-complete decision procedure for non-linear constraints
- Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning
- Politeness and Stable Infiniteness: Stronger Together
- Equational Theorem Proving Modulo
- Unifying Decidable Entailments in Separation Logic with Inductive Definitions
- Subformula Linking for Intuitionistic Logic with Application to Type Theory
- Efficient SAT-based Proof Search in Intuitionistic Propositional Logic
- Proof Search and Certificates for Evidential Transactions
- Non-Clausal Redundancy Properties
- Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
- Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
- Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL Tboxes
- Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance
- A Unifying Splitting Framework
- Integer Induction in Saturation
- Superposition with First-Class Booleans and Inprocessing Clausification
- Superposition for Full Higher-Order Logic
- Implementation and Application
- Making Higher-Order Superposition Work
- Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
- Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
- An Automated Approach to the Collatz Conjecture
- Verified Interactive Computation of Definite Integrals
- ATP and AI
- Confidences for Commonsense Reasoning
- Neural Precedence Recommender
- Improving ENIGMA-Style Clause Selection While Learning From History
- System Descriptions
- A Normative Supervisor for Reinforcement Learning Agents (System Description)
- Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
- The Fusemate Logic Programming System (System Description)
- Twee: An Equational Theorem Prover (System Description)
- The Isabelle/Naproche Natural Language Proof Assistant (System Description)
- The Lean 4 Theorem Prover and Programming Language (System Description)
- Harpoon: Mechanizing Metatheory Interactively (System Description).