Author:Laura Kovács

Keyphrases

Algebraic Recurrences, automated reasoning⁴, automated theorem prover, automated theorem proving², Avatar, AVATAR architecture, clause normal form, consequence finding, first-order logic², first-order theorem prover, first-order theorem proving³, FOOL, fool formula, formal verification, induction², induction with generalization, integer induction, interpolation, invariant generation³, loop, loop invariants, loop synthesis, next state relation, Optimization, polymorphic arrays, program analysis², program verification³, Resolution Calculus, SAT solving, saturation, saturation based proof search, saturation-based theorem proving, static analysis, structural induction, superposition, superposition reasoning, superposition theorem prover, symbol elimination, symbolic computation, term algebra, termination, theorem prover, theorem proving², translation, Vampire³.