Author:Andrei VoronkovPublications 

  EasyChair Preprint no. 12145  EasyChair Preprint no. 12142   EasyChair Preprint no. 10223  EasyChair Preprint no. 9606  EasyChair Preprint no. 9217  EasyChair Preprint no. 8182  EasyChair Preprint no. 6513  EasyChair Preprint no. 5531  EasyChair Preprint no. 5176  EasyChair Preprint no. 5000  EasyChair Preprint no. 2468  EasyChair Preprint no. 3169  EasyChair Preprint no. 3148   EasyChair Preprint no. 826   EasyChair Preprint no. 98  EasyChair Preprint no. 1                    
Keyphrasesautomated deduction, automated induction, automated reasoning^{10}, 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^{6}, firstorder theorem prover, firstorder theorem proving^{6}, FOOL, fool formula, forward subsumption, gaussian variable elimination rule, hereditarily finite sets, induction^{5}, induction with generalization, inductive benchmarks, Inductive data types, integer induction, integers, interpolation, linear arithmetic, logic programming, next state relation, program synthesis^{3}, program verification, proof search, Quantified FirstOrder Logic, recursion, Reducibility constraints, redundancy, Resolution Calculus, runtime algorithm specialization, SAT solving, Satisfiability Modulo Theories^{2}, saturation^{5}, Saturation Algorithms^{3}, saturation based proof search^{3}, saturationbased theorem proving, SMT^{3}, SMT solving, static analysis, structural induction^{2}, Subsumption algorithm, superposition^{5}, superposition calculus, superposition reasoning^{3}, superposition theorem prover, term algebra^{2}, term indexing, theorem prover^{2}, theorem proving^{8}, theory reasoning^{2}, translation, Vampire^{7}, Web Services, Z3. 
