Calculi and Unification
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Non-Disjoint Combined Unification and Closure by Equational Paramodulation
Symbol Elimination and Applications to Parametric Entailment Problems
On the copy complexity of width 3 Horn constraint systems
Description Logics Restricted Unification in the Description Logic FL0
Combining Event Calculus and Description Logic Reasoning via Logic Programming
Semantic Forgetting in Expressive Description Logics
Interactive Theorem Proving Improving Automation for Higher-order Proof Steps
JEFL: Joint Embedding of Formal Proof Libraries
Machine Learning Fast and Slow Enigmas and Parental Guidance
Vampire With a Brain Is a Good ITP Hammer
Satisfiability Modulo Theories Optimization Modulo Non-Linear Arithmetic via Incremental Linearization
Quantifier Simplification by Unification in SMT
Verification Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems
Formal Analysis of Symbolic Authenticity
Formal Verification of a Java Component Using the RESOLVE Framework.