Abstract is missing.
- Choose Your Proofs: Commutativity and Symmetry for Smarter ReasoningAzadeh Farzan. 3-14 [doi]
- Being Polite Is Not Enough (and Other Limits of Theory Combination)Guilherme Vicentin de Toledo, Benjamin Przybocki, Yoni Zohar. 17-34 [doi]
- On Symbol Elimination and Uniform Interpolation in Theory ExtensionsViorica Sofronie-Stokkermans. 35-55 [doi]
- What's Decidable About Arrays With Sums?Roland Herrmann, Philipp Rümmer. 56-74 [doi]
- Cazamariposas: Automated Instability Debugging in SMT-Based Program VerificationYi Zhou 0025, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno. 75-94 [doi]
- Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local SearchEnrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand. 95-115 [doi]
- More is Less: Adding Polynomials for Faster Explanations in NLSATValentin Promies, Jasper Nalbach, Erika Ábrahám, Paul Wagner. 116-135 [doi]
- Ground Truth: Checking Vampire Proofs via Satisfiability Modulo TheoriesMichael Rawson 0001, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel. 136-149 [doi]
- SMT and Functional Equation Solving over the Reals: Challenges from the IMOChad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan. 150-163 [doi]
- Lexicographic Combination of Reduction PairsTeppei Saito, Nao Hirokawa. 167-186 [doi]
- Confluence of Almost Parallel-Closed Generalized Term Rewriting SystemsSalvador Lucas. 187-206 [doi]
- The Computability Path Order for Beta-Eta-Normal Higher-Order RewritingJohannes Niederhauser, Aart Middeldorp. 207-225 [doi]
- Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order RewritingThiago Felicissimo, Jean-Pierre Jouannaud. 226-245 [doi]
- Verified Path IndexingMohamed Chaabani, Simon Robillard. 249-260 [doi]
- Simplified and Verified: A Second Look at a Proof-Producing Union-Find AlgorithmLukas Stevens, Rebecca Ghidini. 261-279 [doi]
- Faithful Logic Embeddings in HOL - Deep and ShallowChristoph Benzmüller. 280-301 [doi]
- A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered ResolutionMartin Bromberger, Martin Desharnais, Christoph Weidenbach. 302-322 [doi]
- Interoperability of Proof Systems with SC-TPTPSimon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak. 325-340 [doi]
- Cut Elimination for Negative Free Logics with Definite DescriptionsAndrzej Indrzejczak. 341-360 [doi]
- From Modal Sequent Calculi to Modal ResolutionDirk Pattinson, Cláudia Nalon, Sourabh Peruri. 361-380 [doi]
- A Fresh Inductive Approach to Useful Call-by-ValuePablo Barenbaum, Delia Kesner, Mariana Milicich. 381-399 [doi]
- Efficient Neural Clause-Selection ReinforcementMartin Suda 0001. 403-422 [doi]
- Learning Conjecturing from ScratchThibault Gauthier, Josef Urban. 423-445 [doi]
- A Theorem Prover Based Approach for SAT-Based Model Checking CertificationGiulia Sindoni, Paolo Pasini, Gianpiero Cabodi, Paolo E. Camurati, Alberto Griggio, Marco Palena, Marco Roveri, Stefano Tonetta. 449-467 [doi]
- Infinite State Model Checking by Learning Transitive RelationsFlorian Frohn, Jürgen Giesl. 468-489 [doi]
- Relatively Complete and Efficient Partial Quantifier EliminationEstifanos Getachew, Arie Gurfinkel, Richard Trefler. 490-507 [doi]
- Computing Witnesses Using the SCAN AlgorithmFabian Achammer, Stefan Hetzl, Renate A. Schmidt. 511-531 [doi]
- Partial Redundancy in SaturationMárton Hajdú, Laura Kovács, Andrei Voronkov. 532-551 [doi]
- Term Ordering DiagramsMárton Hajdú, Robin Coutelier, Laura Kovács, Andrei Voronkov. 552-569 [doi]
- Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOLLukas Bartl, Jasmin Blanchette, Tobias Nipkow. 573-593 [doi]
- Computing Ground Congruence ClassesHendrik Leidinger, Christoph Weidenbach. 594-613 [doi]
- Anti-pattern TemplatesJan Otop. 614-631 [doi]
- Equational Reasoning Modulo Commutativity in Languages with BindersAli K. Caires-Santos, Maribel Fernández, Daniele Nantes Sobrinho. 632-652 [doi]
- Uniform Interpolation and Forgetting for Large-Scale Ontologies with Application to Semantic Difference in SNOMED CTYizheng Zhao, Junyi Zhang, Renate A. Schmidt. 655-675 [doi]
- Concrete Domains Meet Expressive Cardinality Restrictions in Description LogicsFranz Baader, Stefan Borgwardt, Filippo De Bortoli, Patrick Koopmann. 676-695 [doi]
- A Real-Analytic Approach to Differential-Algebraic Dynamic LogicJonathan Hellwig, André Platzer. 696-714 [doi]
- Entailment vs. Verification for Partial-Assignment Satisfiability and EnumerationRoberto Sebastiani. 717-735 [doi]
- Unfolding Boxes with Local ConstraintsLong Qian, Eric Wang, Bernardo Subercaseaux, Marijn J. H. Heule. 736-754 [doi]