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