ABSTRACT. We recently extended the saturation program synthesis framework to synthesize recursive functions. In this contribution, we present a detailed study of how our framework synthesizes the floored division function.

ABSTRACT. Runtime code specialization makes functions that are often evaluated with a certain fixed parameter faster by creating and calling a specialized function where this fixed parameter is partially evaluated. For example, Vampire employs such an approach for term matching from an index and comparing terms under a substitution. Despite the increase in efficiency, this comes at the price of having to execute interpreted code, which is often much slower than compiled and optimised code. In this work, we take a look at how this execution can be made faster.

ABSTRACT. Most first-order theorem provers use saturation as their main proof search strategy. Such a method generates a large number of clauses, which can be prohibitive for solving difficult theorems. Furthermore, checking whether a clause is redundant can be as hard as proving the theorem itself. This is why there exists sufficient redundancy criteria that are easier to check. In particular, this talk will discuss the NP-Complete subsumption and subsumption resolution rules. We will discuss a practical SAT-based implementation in the Vampire theorem prover, and how heuristics can significantly improve the performance of these rules. We first discuss strong and cheap pruning methods for both subsumption and subsumption resolution. Then, we introduce a simple Machine Learning method to choose the best encoding for subsumption resolution. Finally, we discuss the impact of using a cutoff to prevent the SAT solver to run for too long.