Author:Andrei Voronkov

Keyphrases

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 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.