| ||||
| ||||
![]() Title:Hints for AVATAR Authors:Martin Suda Conference:Vampire 2019 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. Hints for AVATAR ![]() Hints for AVATAR | ||||
Copyright © 2002 – 2025 EasyChair |