Abstract is missing.
- Non-well-founded Deduction for Induction and CoinductionLiron Cohen 0001. 3-24 [doi]
- Towards the Automatic MathematicianMarkus N. Rabe, Christian Szegedy. 25-37 [doi]
- Tableau-based Decision Procedure for Non-Fregean Logic of Sentential IdentityJoanna Golinska-Pilarek, Taneli Huuskonen, Michal Zawidzki. 41-57 [doi]
- Learning from Łukasiewicz and Meredith: Investigations into Proof StructuresChristoph Wernhard, Wolfgang Bibel. 58-75 [doi]
- Efficient Local Reductions to Basic Modal LogicFabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon. 76-92 [doi]
- Isabelle's Metalogic: Formalization and Proof CheckerTobias Nipkow, Simon Roßkopf. 93-110 [doi]
- The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear ConstraintsFranz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller. 113-130 [doi]
- Universal Invariant Checking of Parametric Systems with Quantifier-free SMT ReasoningAlessandro Cimatti, Alberto Griggio, Gianluca Redondi. 131-147 [doi]
- Politeness and Stable Infiniteness: Stronger TogetherYing Sheng 0007, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli. 148-165 [doi]
- Equational Theorem Proving ModuloDohan Kim 0001, Christopher Lynch. 166-182 [doi]
- Unifying Decidable Entailments in Separation Logic with Inductive DefinitionsMnacho Echenim, Radu Iosif, Nicolas Peltier. 183-199 [doi]
- Subformula Linking for Intuitionistic Logic with Application to Type TheoryKaustuv Chaudhuri. 200-216 [doi]
- Efficient SAT-based Proof Search in Intuitionistic Propositional LogicCamillo Fiorentini. 217-233 [doi]
- Proof Search and Certificates for Evidential TransactionsVivek Nigam, Giselle Reis, Samar Rahmouni, Harald Ruess. 234-251 [doi]
- Non-clausal Redundancy PropertiesLee A. Barnett, Armin Biere. 252-272 [doi]
- Multi-Dimensional Interpretations for Termination of Term RewritingAkihisa Yamada 0002. 273-290 [doi]
- Finding Good Proofs for Description Logic Entailments using Recursive Quality MeasuresChristian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova. 291-308 [doi]
- EL TBoxesFranz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah. 309-326 [doi]
- Generalized Completeness for SOS Resolution and its Application to a New Notion of RelevanceFajar Haifani, Sophie Tourret, Christoph Weidenbach. 327-343 [doi]
- A Unifying Splitting FrameworkGabriel Ebner, Jasmin Blanchette, Sophie Tourret. 344-360 [doi]
- Integer Induction in SaturationPetra Hozzová, Laura Kovács, Andrei Voronkov. 361-377 [doi]
- Superposition with First-class Booleans and Inprocessing ClausificationVisa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic. 378-395 [doi]
- Superposition for Full Higher-order LogicAlexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic. 396-412 [doi]
- Making Higher-Order Superposition WorkPetar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret. 415-432 [doi]
- Dual Proof Generation for Quantified Boolean Formulas with a BDD-based SolverRandal E. Bryant, Marijn J. H. Heule. 433-449 [doi]
- Reliable Reconstruction of Fine-grained Proofs in a Proof AssistantHans-Jörg Schurr, Mathias Fleury, Martin Desharnais. 450-467 [doi]
- An Automated Approach to the Collatz ConjectureEmre Yolcu, Scott Aaronson, Marijn J. H. Heule. 468-484 [doi]
- Verified Interactive Computation of Definite IntegralsRunqing Xu, Liming Li, Bohua Zhan. 485-503 [doi]
- Confidences for Commonsense ReasoningTanel Tammet, Dirk Draheim, Priit Järv. 507-524 [doi]
- Neural Precedence RecommenderFilip Bártek, Martin Suda 0001. 525-542 [doi]
- Improving ENIGMA-style Clause Selection while Learning From HistoryMartin Suda 0001. 543-561 [doi]
- A Normative Supervisor for Reinforcement Learning AgentsEmery Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori. 565-576 [doi]
- Automatically Building Diagrams for Olympiad Geometry ProblemsRyan Krueger, Jesse Michael Han, Daniel Selsam. 577-588 [doi]
- The Fusemate Logic Programming SystemPeter Baumgartner 0001. 589-601 [doi]
- Twee: An Equational Theorem ProverNicholas Smallbone. 602-613 [doi]
- The Isabelle/Naproche Natural Language Proof AssistantAdrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel. 614-624 [doi]
- The Lean 4 Theorem Prover and Programming LanguageLeonardo de Moura, Sebastian Ullrich. 625-635 [doi]
- Harpoon: Mechanizing Metatheory Interactively - (System Description)Jacob Errington, Junyoung Jang, Brigitte Pientka. 636-648 [doi]