Author name cluster

Johannes Schoisswohl

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

LPAR Conference 2024 Conference Paper

VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

Johannes Schoisswohl
Laura Kovács
Konstantin Korovin

We introduce Virtual Integer-Real Arithmetic Substitution (Viras), a quantifier elim- ination procedure for deciding quantified linear mixed integer-real arithmetic problems. Viras combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that Viras gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

Details

LPAR Conference 2023 Conference Paper

Refining Unification with Abstraction

Ahmed Bhayat
Konstantin Korovin
Laura Kovács
Johannes Schoisswohl

Automated reasoning with theories and quantifiers is a common demand in formal methods. A major challenge that arises in this respect comes with rewriting/simplifying terms that are equal with respect to a background first-order theory T, as equality reasoning in this context requires unification modulo T. We introduce a refined algorithm for unification with abstraction in T, allowing for a fine-grained control of equality constraints and substitutions introduced by standard unification with abstraction approaches. We experimentally show the benefit of our approach within first-order linear rational arithmetic.

Details

LFMTP Workshop 2021 Workshop Paper

Automating Induction by Reflection

Johannes Schoisswohl
Laura Kovács

Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The reason for that is that in first-order logic induction requires an infinite number of axioms, which is not a feasible input to a computer-aided theorem prover requiring a finite input. Mathematical practice is to specify these infinite sets of axioms as axiom schemes. Unfortunately these schematic definitions cannot be formalized in first-order logic, and therefore not supported as inputs for first-order theorem provers. In this work we introduce a new method, inspired by the field of axiomatic theories of truth, that allows to express schematic inductive definitions, in the standard syntax of multi-sorted first-order logic. Further we test the practical feasibility of the method with state-of-the-art theorem provers, comparing it to solvers' native techniques for handling induction.

Details DOI