Author:Andrei Voronkov

Keyphrases

automated deduction, automated induction, automated reasoning⁹, automated theorem prover, automated theorem proving², Avatar³, AVATAR architecture², bounded quantifiers, Clausal Normal Form, clause normal form, Clausification, code trees, computability, conference management, easychair, first-order logic⁶, first-order theorem prover, first-order theorem proving⁵, FOOL, fool formula, forward subsumption, gaussian variable elimination rule, hereditarily finite sets, induction³, induction with generalization, inductive benchmarks, Inductive data types, integer induction, integers, interpolation, logic programming, next state relation, program synthesis, program verification, proof search, Resolution Calculus, runtime algorithm specialization, SAT solving, Satisfiability Modulo Theories², saturation, Saturation Algorithms³, saturation based proof search³, saturation-based theorem proving, SMT², SMT solving, static analysis, structural induction², Subsumption algorithm, superposition, superposition calculus, superposition reasoning³, superposition theorem prover, term algebra², term indexing, theorem prover², theorem proving⁵, theory reasoning², translation, Vampire⁷, Web Services, Z3.