Automated Deduction - CADE 28 : : 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.12699 |
---|---|
: | |
TeilnehmendeR: | |
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
|
Online Access: | |
Physical Description: | 1 online resource (655 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
LEADER | 11237nam a22004693i 4500 | ||
---|---|---|---|
001 | 5006676599 | ||
003 | MiAaPQ | ||
005 | 20240229073842.0 | ||
006 | m o d | | ||
007 | cr cnu|||||||| | ||
008 | 240229s2021 xx o ||||0 eng d | ||
020 | |a 9783030798765 |q (electronic bk.) | ||
020 | |z 9783030798758 | ||
035 | |a (MiAaPQ)5006676599 | ||
035 | |a (Au-PeEL)EBL6676599 | ||
035 | |a (OCoLC)1260840749 | ||
040 | |a MiAaPQ |b eng |e rda |e pn |c MiAaPQ |d MiAaPQ | ||
050 | 4 | |a Q334-342 | |
100 | 1 | |a Platzer, André. | |
245 | 1 | 0 | |a Automated Deduction - CADE 28 : |b 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. |
250 | |a 1st ed. | ||
264 | 1 | |a Cham : |b Springer International Publishing AG, |c 2021. | |
264 | 4 | |c {copy}2021. | |
300 | |a 1 online resource (655 pages) | ||
336 | |a text |b txt |2 rdacontent | ||
337 | |a computer |b c |2 rdamedia | ||
338 | |a online resource |b cr |2 rdacarrier | ||
490 | 1 | |a Lecture Notes in Computer Science Series ; |v v.12699 | |
505 | 0 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a An Automated Approach to the Collatz Conjecture. | |
588 | |a Description based on publisher supplied metadata and other sources. | ||
590 | |a Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. | ||
655 | 4 | |a Electronic books. | |
700 | 1 | |a Sutcliffe, Geoff. | |
776 | 0 | 8 | |i Print version: |a Platzer, André |t Automated Deduction - CADE 28 |d Cham : Springer International Publishing AG,c2021 |z 9783030798758 |
797 | 2 | |a ProQuest (Firm) | |
830 | 0 | |a Lecture Notes in Computer Science Series | |
856 | 4 | 0 | |u https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6676599 |z Click to View |