Abstract is missing.
- Efficient Automated Reasoning About Sets and Multisets with Cardinality ConstraintsRuzica Piskac. 3-10 [doi]
- An SMT Theory of Fixed-Point ArithmeticMarek S. Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamaric. 13-31 [doi]
- Covered Clauses Are Not Propagation RedundantLee A. Barnett, David Cerna, Armin Biere. 32-47 [doi]
- The Resolution of Keller's ConjectureJoshua Brakensiek, Marijn Heule, John Mackey, David Narváez. 48-65 [doi]
- How QBF Expansion Makes Strategy Extraction HardLeroy Chew, Judith Clymo. 66-82 [doi]
- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference PredicatesEmanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti. 83-102 [doi]
- Solving Bitvectors with MCSAT: Explanations from Bits and PiecesStéphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre. 103-121 [doi]
- Monadic Decomposition in Integer Linear ArithmeticMatthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu. 122-140 [doi]
- Scalable Algorithms for Abduction via Enumerative Syntax-Guided SynthesisAndrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli. 141-160 [doi]
- Deciding the Word Problem for Ground Identities with Commutative and Extensional SymbolsFranz Baader, Deepak Kapur. 163-180 [doi]
- Combined Covers and Beth DefinabilityDiego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin. 181-200 [doi]
- Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of SuperpostulatesTimm Lampert, Anderson Nakano. 201-217 [doi]
- A Decision Procedure for String to Code Point ConversionAndrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli. 218-237 [doi]
- Politeness for the Theory of Algebraic DatatypesYing Sheng 0007, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett. 238-255 [doi]
- A Knuth-Bendix-Like Ordering for Orienting Combinator EquationsAhmed Bhayat, Giles Reger. 259-277 [doi]
- A Combinator-Based Superposition Calculus for Higher-Order LogicAhmed Bhayat, Giles Reger. 278-296 [doi]
- Subsumption Demodulation in First-Order Theorem ProvingBernhard Gleiss, Laura Kovács, Jakob Rath. 297-315 [doi]
- A Comprehensive Framework for Saturation Theorem ProvingUwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. 316-334 [doi]
- Possible Models Computation and Revision - A Practical ApproachPeter Baumgartner 0001. 337-355 [doi]
- SGGS Decision ProceduresMaria Paola Bonacina, Sarah Winkler. 356-374 [doi]
- Integrating Induction and Coinduction via Closure Operators and Proof CyclesLiron Cohen 0001, Reuben N. S. Rowe. 375-394 [doi]
- Logic-Independent Proof Search in Logical Frameworks - (Short Paper)Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer. 395-401 [doi]
- Layered Clause Selection for Theory Reasoning - (Short Paper)Bernhard Gleiss, Martin Suda 0001. 402-409 [doi]
- Description Logics with Concrete Domains and General Concept Inclusions RevisitedFranz Baader, Jakub Rydval. 413-431 [doi]
- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic LogicDavid A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider 0001, Dmitriy Traytel. 432-453 [doi]
- Constructive Hybrid GamesBrandon Bohrer, André Platzer. 454-473 [doi]
- Formalizing a Seligman-Style Tableau System for Hybrid Logic - (Short Paper)Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen. 474-481 [doi]
- NP Reasoning in the Monotone μ-CalculusDaniel Hausmann 0001, Lutz Schröder. 482-499 [doi]
- Soft Subexponentials and MultiplexingMax I. Kanovich, Stepan Kuznetsov, Vivek Nigam, Andre Scedrov. 500-517 [doi]
- Mechanised Modal Model TheoryYiming Xu, Michael Norrish. 518-533 [doi]