Lambda-Superposition: From Theory to Trophy (abstract)

Verification of NP-hardness for Exact Lattice Problems (abstract)

Verified Given Clause Procedures (abstract)

An Isabelle/HOL Formalization of the SCL(FOL) Calculus (abstract)

Theorem Proving in Dependently-Typed Higher-Order Logic (abstract)

Reasoning about Regular Properties: A Comparative Study (abstract)

A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification (abstract)

Formal Reasoning about Influence in Natural Sciences Experiments (abstract)

An Experimental Pipeline for Automated Reasoning in Natural Language (abstract)

Proving Non-Termination by Acceleration Driven Clause Learning – Short Paper (abstract)

Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs (abstract)

Proving Termination of C Programs with Lists (abstract)

Left-Linear Completion with AC Axioms (abstract)

Automated Reasoning with Data

A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus (abstract)

Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic (abstract)

Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory (abstract)

COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (abstract)

Iscalc: an Interactive Symbolic Computation Framework (System Description) (abstract)

Confluence Criteria for Logically Constrained Rewrite Systems (abstract)

Towards Fast Nominal Anti-Unification of Letrec-Expressions (abstract)

Incremental Rewriting Modulo SMT (abstract)

SAT-Based Subsumption Resolution (abstract)

Certified Core-Guided MaxSAT Solving (abstract)

A more Pragmatic CDCL for IsaSAT and targetting LLVM (abstract)

How Can We Make Trustworthy AI? (abstract)

Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness (abstract)

Choose your Colour: Tree Interpolation for Quantified Formulas in SMT (abstract)

QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment (abstract)

On Incremental Pre-processing for SMT (abstract)

Decidability of difference logic over the reals with uninterpreted unary predicates (abstract)

On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$ (abstract)

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs (abstract)

Nominal Techniques for Software Specification and Verification (abstract)

Superposition with Delayed Unification (abstract)

Program Synthesis in Saturation (abstract)

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning (abstract)