Author:Johannes Schoisswohl

Keyphrases

arithmetic², automated reasoning⁷, automated theorem provers, automated theorem proving², AVATAR architecture, Benchmarks², decision procedure, Descision Procedure, first-order logic, first-order theorem proving³, gaussian variable elimination rule, Hyperproperties², induction, induction with generalization, inductive benchmarks, Inductive data types, integers, LIA, linear arithmetic⁴, LIRA², literal selection², logic, LRA, model checking², Presburger arithmetic, proof search, Quantified First-Order Logic, quantifier elimination², real arithmetic², redundancy², saturation based proof search², simplification, SMT⁸, software verification², structural induction, superposition², superposition reasoning, term algebra, theorem prover, theorem proving, theory reasoning, unification, Unification with Abstraction, Vampire, virtual substitution.