Custom cover image
Automated reasoning : 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings : Part I / Christoph Benzmüller, Marijn J.H. Heule, Renate A. Schmidt, editors
Contributor(s): Resource type: Ressourcentyp: Buch (Online)Book (Online)Language: English Series: Lecture notes in artificial intelligence | Lecture notes in computer science ; 14739Publisher: Cham : Springer, 2024Description: 1 Online-Ressource (xvi, 482 pages) : illustrations (some color)ISBN:- 9783031634987
- IJCAR 2024
- 511.3/6028563 23/eng/20240711
- QA76.9.A96
Contents:
Summary: This two-volume set of LNAI 14739-14740 constitute the proceedings of the 12th International Joint Conference on Automated Reasoning, IJCAR 2024, held in Nancy, France, during July 3-6, 2024. The 39 full research papers and 6 short papers presented in this book were carefully reviewed and selected from 115 submissions. The papers focus on the following topics: theorem proving and tools; SAT, SMT and Quantifier Elimination; Intuitionistic Logics and Modal Logics; Calculi, Proof Theory and Decision Procedures; and Unification, Rewriting and Computational Models. This book is open accessPPN: PPN: 1938156641Package identifier: Produktsigel: ZDB-94-OAB
Intro -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Contributions -- Automated Reasoning for Mathematics -- 1 The Origins and Foundations of Automated Reasoning -- 2 Taking Stock -- 3 A Personal History -- 4 Domain-General Reasoning for Verification -- 5 Domain-Specific Reasoning for Verification -- 6 Automation for the Discovery of New Theorems -- 7 Machine Learning and Symbolic AI -- 8 Conclusions -- References -- Induction in Saturation -- 1 Introduction -- 2 Induction in Saturation -- In a Nutshell -- 3 Induction and Arithmetic -- 4 Induction over Arrays
5 Induction over Lists -- 6 Conclusions and Outlook -- References -- Stepping Stones in the TPTP World -- 1 Introduction -- 2 The TPTP Language -- 3 The TPTP Problem Library -- 4 The TSTP Solution Library -- 5 The SZS Ontologies -- 6 Specialist Problem Classes -- 7 Problem Difficulty Ratings -- 8 SystemOnTPTP and StarExec -- 9 The CADE ATP System Competition -- 10 TPTP World Users -- 11 Conclusion -- References -- Theorem Proving and Tools -- An Empirical Assessment of Progress in Automated Theorem Proving -- 1 Introduction -- 2 The TPTP Problem Library -- 2.1 Specialist Problem Classes
2.2 TPTP Problem Ratings -- 3 The TSTP Solution Library -- 3.1 Resource Limits -- 4 Analysis Processes -- 4.1 Analysis Data -- 4.2 Coherent SPC Sets -- 4.3 Six Analyses -- 5 Evidence of Progress -- 5.1 First Solutions -- 5.2 Solutions and Ratings -- 6 Conclusion -- References -- A Higher-Order Vampire (Short Paper) -- 1 Introduction -- 2 Preliminaries -- 3 Calculus -- 4 Implementation -- 5 Strategies and the Schedule -- 6 Related Work -- 7 Conclusion -- References -- Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 HOL
2.2 DHOL -- 2.3 Erasure -- 3 Tableau Calculus for DHOL -- 3.1 Rules -- 3.2 Soundness and Completeness -- 4 Implementation -- 4.1 Type Checking -- 4.2 Implementation of the Rules -- 4.3 Generating Instantiations -- 5 Case Study: List Reversal Is an Involution -- 6 Conclusion -- References -- The Naproche-ZF Theorem Prover (Short Paper) -- 1 Introduction -- 2 Controlled Natural Language -- 3 Semantics and Proof Checking -- 4 Conclusion and Future Work -- References -- Reducibility Constraints in Superposition -- 1 Introduction -- 2 Preliminaries -- 3 Reducibility Constraints
4 Model Construction in BLINC -- 5 Redundancy Detection in BLINC -- 6 Evaluation -- 7 Related Work -- 8 Conclusions -- References -- First-Order Automatic Literal Model Generation -- 1 Introduction -- 2 Preliminaries -- 3 SCL: Clause Learning from Simple Models -- 4 Generating Models -- 5 Conclusion and Future Work -- References -- Synthesis of Recursive Programs in Saturation -- 1 Introduction -- 2 Preliminaries -- 3 Recent Developments in Saturation -- 4 Saturation with Induction in Constructive Logic -- 5 Induction with Magic Formulas -- 6 Programs with Primitive Recursion
No physical items for this record
Open access
Open Access