Showing cs.LOShow all
2 papers · 1 filter
cs.LO2024
One is all you need: Second-order Unification without First-order Variables
David M. Cerna, Julian Parsert
We introduce a fragment of second-order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable…
cs.LO2024
Linear Programming in Isabelle/HOL
Julian Parsert
Linear programming describes the problem of optimising a linear objective function over a set of constraints on its variables. In this paper we present a solver for linear programs…