Author:Johannes Schoisswohl

EasyChair Preprint no. 13150
EasyChair Preprint no. 9606
EasyChair Preprint no. 5531
EasyChair Preprint no. 5000
EasyChair Preprint no. 2468


arithmetic2, automated reasoning5, automated theorem proving, AVATAR architecture, decision procedure, Descision Procedure, first-order logic, first-order theorem proving, gaussian variable elimination rule, induction, induction with generalization, inductive benchmarks, Inductive data types, integers, LIA, linear arithmetic2, LIRA2, logic, LRA, Presburger arithmetic, proof search, Quantified First-Order Logic, quantifier elimination2, saturation based proof search2, SMT4, structural induction, superposition reasoning, term algebra, theorem prover, theorem proving, theory reasoning, unification, Unification with Abstraction, Vampire, virtual substitution.