Author:Johannes Schoisswohl

Publications
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic Johannes Schoisswohl, Laura Kovács and Konstantin Korovin In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Refining Unification with Abstraction Ahmed Bhayat, Konstantin Korovin, Laura Kovacs and Johannes Schoisswohl In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint 13150
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint 13150
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
Inductive Benchmarks for Automated Reasoning Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 5531
Making Theory Reasoning Simpler Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 5000
Induction with Generalization in Superposition Reasoning Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 2468
Induction with Generalization in Superposition Reasoning Petra Hozzová, Laura Kovács, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 2468

Keyphrases

arithmetic², automated reasoning⁵, 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 arithmetic², LIRA², logic, LRA, Presburger arithmetic, proof search, Quantified First-Order Logic, quantifier elimination², saturation based proof search², SMT⁴, structural induction, superposition reasoning, term algebra, theorem prover, theorem proving, theory reasoning, unification, Unification with Abstraction, Vampire, virtual substitution.