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