2 citations · 2 across the 2 of their papers we have counts for
3 papers
cs.LO2022★ 2 cited
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Martin Bromberger, Irina Dragoste, Rasha Faqeh +6
In a previous paper, we have shown that clause sets belonging to the Horn Bernays-Schönfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clau…
cs.LO2021
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Martin Bromberger, Irina Dragoste, Rasha Faqeh +3
The Bernays-Schönfinkel first-order logic fragment over simple linear real arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR) clause sets with both univ…
cs.LO2018
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Martin Bromberger
We present a combination of the Mixed-Echelon-Hermite transformation and the Double-Bounded Reduction for systems of linear mixed arithmetic that preserve satisfiability and can be…