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.