AVATAR: The Architecture for First-Order Theorem Provers
CAV, pp. 696-710, 2014.
This paper describes a new architecture for first-order resolution and superposition theorem provers called AVATAR (Advanced Vampire Architecture for Theories and Resolution). Its original motivation comes from a problem well-studied in the past dealing with problems having clauses containing propositional variables and other clauses th...More
PPT (Upload PPT)