Author:Andrei VoronkovPublications 

EasyChair Preprint no. 3169  EasyChair Preprint no. 3148   EasyChair Preprint no. 2468  EasyChair Preprint no. 826   EasyChair Preprint no. 98  EasyChair Preprint no. 1                    
Keyphrasesautomated induction, automated reasoning^{5}, automated theorem prover, automated theorem proving^{2}, Avatar^{3}, AVATAR architecture^{2}, bounded quantifiers, Clausal Normal Form, clause normal form, Clausification, code trees, computability, conference management, easychair, firstorder logic^{5}, firstorder theorem prover, firstorder theorem proving^{3}, FOOL, fool formula, forward subsumption, hereditarily finite sets, induction, induction with generalization, interpolation, logic programming, next state relation, program verification, Resolution Calculus, runtime algorithm specialization, SAT solving, Satisfiability Modulo Theories^{2}, Saturation Algorithms^{3}, saturation based proof search, SMT, SMT solving, static analysis, structural induction, Subsumption algorithm, superposition, superposition calculus, superposition reasoning, term algebra, term indexing, theorem prover, theorem proving^{4}, theory reasoning, translation, Vampire^{6}, Web Services, Z3. 
