Tags:AVATAR, Saturation-based proving, theorem proving and Vampire
Abstract:
The use of the AVATAR architecture within first-order theorem prover turns the work of the saturation core on a single monolithic problem into a sequence of simpler related sub-problems. We use the hints method for clause prioritisation to prefer selection of those clauses which already appeared in the proof of previous sub-problems. Based on the assumptions that the individual sub-problems tend to be related, this approach facilitates learning from past experience. In the talk I will describe the implementation of the idea in the automatic theorem prover Vampire and report on experimental results.