Invited Paper
Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints
SAT; SMT and QBF
An SMT Theory of Fixed-Point Arithmetic
Covered Clauses Are Not Propagation Redundant
The Resolution of Kellers Conjecture
How QBF Expansion Makes Strategy Extraction Hard
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Solving bit-vectors with MCSAT: explanations from bits and pieces
Monadic Decomposition in Integer Linear Arithmetic
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
Decision Procedures and Combination of Theories
Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Combined Covers and Beth Definability
Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates
A Decision Procedure for String to Code Point Conversion
Politeness for The Theory of Algebraic Datatypes
Superposition
A Knuth-Bendix-Like Ordering for Orienting Combinator Equations
A Combinator-Based Superposition Calculus for Higher-Order Logic
Subsumption Demodulation in First-Order Theorem Proving
A Comprehensive Framework for Saturation Theorem Proving
Proof Procedures
Possible Models Computation and Revision
A Practical Approach
SGGS Decision Procedures
Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Logic-Independent Proof Search in Logical Frameworks (short paper)
Layered Clause Selection for Theory Reasoning (short paper)
Non Classical Logics
Description Logics with Concrete Domains and General Concept Inclusions Revisited
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Constructive Hybrid Games
Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
NP Reasoning in the Monotone µ-Calculus
Soft subexponentials and multiplexing
Mechanised Modal Model Theory.