RAPID now comes equipped with a new verification mode - the lemmaless mode - that delegates inductive reasoning in the underlying first-order theorem prover without instantiating trace lemmas. Specifically we noticed that recent developments in automating induction in first-order provers could be used to prove some mathematical theorems over integers that require induction. We leverage these extended rules in the superposition calculus and introduce induction in the first-order theorem prover over trace logic timepoints. 

This approach allows to overcome two main limitations of trace lemmas:

1. Trace lemmas are manually identified common inductive patterns, as induction is not expressible in first-order logic. However, this means that proof search is majorly limited to identified trace lemmas, and the effectiveness of first-order reasoning depends on the expressiveness of manually supplied lemmas. 
2. Trace lemmas are automatically instantiated for all appropriate inductive program variables, i.e. with the size of the program, the amount of used inductive lemmas that are automatically added to the input set also rapidly increases, which in turn increases the search space and slows down proof search. 

To overcome these limitations, we introduce inductive inferences over timepoints and find inductive conclusions during proof search that allow to prove an even bigger subset of our input examples.  Specifically, we add two new inference rules to the underlying prover: 

• Multi-clause goal induction: intuitively, many quantified safety properties are almost inductive and thus are structurally similar to the required loop invariant to obtain a proof. We leverage this fact by making sure we use clauses containing timepoints that stem from the safety property we want to prove in the first place. That is, inductive parts of the proof search are immediately property/goal-directed and thus can significantly speed up proof search. 
• Array-mapping induction: doing induction based on clauses stemming from the safety property is not always enough, since these properties do not necessarily have to be inductive for the loops of a program. For example, one could have a program containing two consecutive loops, one incrementing each element of an array, while the other one decrements each element. If we wanted to prove that the array after the execution of both loops is exactly the same as before running the program, then this is not an inductive property for the two loops. In other words, induction inferences on this property will not lead to inductive conclusions that will abstract the right loop behaviour. This means we need to have inductive inferences on clauses stemming from the two loops to find the right loop invariants for each of the loops. This is where array-mapping induction comes into play. 

This approach has promising results: from 111 input problems, we could successfully solve 93 benchmarks fully automatically, while our prior approach could only solve 78 of these benchmarks. For details check out our preprint paper about lemmaless induction in the RAPID framework at https://github.com/vprover/vampire_publications/blob/master/paper_draft…