ABSTRACT. Propositional satisfiability is the problem of determining, for a formula of propositional logic, whether there is an assignment of truth values to its variables for which that formula evaluates to true. In the 90's, a technology called SAT solving became impressively powerful, being able to check the satisfiability of huge real-world propositional logic problems with millions of clauses.

Based on this success, the question was raised whether these technologies could be somehow extended to check also quantifier-free first-order logic formulas over different theories for satisfiability. This would be very helpful as a lot of real-world problems cannot be conveniently encoded in propositional logic. This was the motivation for the development of so-called Satisfiability Modulo Theories (SMT) solvers.

In this talk, we review the algorithmic background of these developments for arithmetic theories, present our own SMT solver SMT-RAT and discuss interesting future research directions.

ABSTRACT. We present a generic method to configure an automated reasoning solver in order to increase its performance on selected target problems. We describe a strategy invention system Grackle that is designed to invent a set of strong and complementary solver strategies. The strategies are then used to train a decision tree model to select the best strategy for a specific input problem. We evaluate our method on the SMT solver Bitwuzla and we obtain a decent increase in the number of solved problems, and a substantial decrease in runtime.

ABSTRACT. We introduce decomposition rules. They are a family of axiom schemata that are instantiated at run-time to add new axioms to a logical theory. These new axioms are implications, whose preconditions will be constructed from an analysis of the goal to be proved and the theory in which it is to be proved. We illustrate their use in the FRANK query answering system.

ABSTRACT. We present a novel approach to automate the verification of first-order inductive program properties capturing the partial correctness of imperative program loops with branching, integers and arrays. We rely on trace logic, an instance of first-order logic with theories, to express first-order program semantics by quantifying over program execution timepoints. Program verification in trace logic is translated into a first-order theorem proving problem where, to date, effective reasoning has required the introduction of so-called trace lemmas to establish inductive properties. In this work, we extend trace logic with generic induction schemata over timepoints and loop counters, reducing reliance on trace lemmas. Inferring and proving loop invariants becomes an inductive inference step within superposition-based first-order theorem proving. We implemented our approach in the RAPID framework, using the first-order theorem prover VAMPIRE. Our extensive experimental analysis show that automating inductive verification in trace logic improves over existing approaches.

ABSTRACT. The Kruskal-Katona theorem is a celebrated result of extremal combinatorics providing precise cardinality bounds on the `shadow' of a family of finite sets: the family given by removing an element from each set of the original. We describe a formalization of the Kruskal-Katona theorem in the Lean theorem prover, including a computable implementation of the shadow as well as standard inequalities about it, and a definition of the colexicographic ordering on finite sets. In addition, we apply these results to other classical combinatorial theorems: Sperner's theorem on antichains and the Erdős-Ko-Rado theorem on intersecting families.