Abstract is missing.
- Certified Core-Guided MaxSAT SolvingJeremias Berg, Bart Bogaerts 0001, Jakob Nordström, Andy Oertel, Dieter Vandesande. 1-22 [doi]
- Superposition with Delayed UnificationAhmed Bhayat, Johannes Schoisswohl, Michael Rawson 0001. 23-40 [doi]
- On Incremental Pre-processing for SMTNikolaj Bjørner, Katalin Fazekas. 41-60 [doi]
- Verified Given Clause ProceduresJasmin Blanchette, Qi Qiu, Sophie Tourret. 61-77 [doi]
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and AssignmentMaria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier. 78-95 [doi]
- Uniform Substitution for Dynamic Logic with Communicating Hybrid ProgramsMarvin Brieger, Stefan Mitsch, André Platzer. 96-115 [doi]
- An Isabelle/HOL Formalization of the SCL(FOL) CalculusMartin Bromberger, Martin Desharnais, Christoph Weidenbach. 116-133 [doi]
- SCL(FOL) Can Simulate Non-Redundant Superposition Clause LearningMartin Bromberger, Chaahat Jain, Christoph Weidenbach. 134-152 [doi]
- Formal Reasoning About Influence in Natural Sciences ExperimentsFlorian Bruse, Martin Lange, Sören Möller. 153-169 [doi]
- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)Yu-Fang Chen 0001, Philipp Rümmer, Wei-Lun Tsai. 170-189 [doi]
- SAT-Based Subsumption ResolutionRobin Coutelier, Laura Kovács, Michael Rawson 0001, Jakob Rath. 190-206 [doi]
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)Mathias Fleury, Peter Lammich. 207-219 [doi]
- Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)Florian Frohn, Jürgen Giesl. 220-233 [doi]
- COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description)Oliver Görlitz, Daniel Hausmann 0001, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder. 234-247 [doi]
- Choose Your Colour: Tree Interpolation for Quantified Formulas in SMTElisabeth Henkel, Jochen Hoenicke, Tanja Schindler. 248-265 [doi]
- Proving Termination of C Programs with ListsJera Hensel, Jürgen Giesl. 266-285 [doi]
- Reasoning About Regular Properties: A Comparative StudyTomás Fiedor, Lukás Holík, Martin Hruska, Adam Rogalewicz, Juraj Síc, Pavol Vargovcík. 286-306 [doi]
- Program Synthesis in SaturationPetra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov. 307-324 [doi]
- A Uniform Formalisation of Three-Valued Logics in Bisequent CalculusAndrzej Indrzejczak, Yaroslav I. Petrukhin. 325-343 [doi]
- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency PairsJan-Christoph Kassing, Jürgen Giesl. 344-364 [doi]
- Verification of NP-Hardness Reduction Functions for Exact Lattice ProblemsKatharina Kreuzer, Tobias Nipkow. 365-381 [doi]
- Buy One Get 14 Free: Evaluating Local Reductions for Modal LogicCláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon. 382-400 [doi]
- Left-Linear Completion with AC AxiomsJohannes Niederhauser, Nao Hirokawa, Aart Middeldorp. 401-418 [doi]
- +Dennis Peuter, Viorica Sofronie-Stokkermans, Sebastian Thunert. 419-437 [doi]
- Theorem Proving in Dependently-Typed Higher-Order LogicColin Rothgang, Florian Rabe 0001, Christoph Benzmüller. 438-455 [doi]
- Towards Fast Nominal Anti-unification of Letrec-ExpressionsManfred Schmidt-Schauß, Daniele Nantes Sobrinho. 456-473 [doi]
- Confluence Criteria for Logically Constrained Rewrite SystemsJonas Schöpf, Aart Middeldorp. 474-490 [doi]
- Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set TheoryLukas Stevens. 491-508 [doi]
- An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper)Tanel Tammet, Priit Järv, Martin Verrev, Dirk Draheim. 509-521 [doi]
- Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and PolitenessGuilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett. 522-541 [doi]
- Decidability of Difference Logic over the Reals with Uninterpreted Unary PredicatesBernard Boigelot, Pascal Fontaine, Baptiste Vergain. 542-559 [doi]
- Incremental Rewriting Modulo SMTGerald Whitters, Vivek Nigam, Carolyn L. Talcott. 560-576 [doi]
- Iscalc: An Interactive Symbolic Computation Framework (System Description)Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu. 577-589 [doi]