3 citations · 3 across the 5 of their papers we have counts for
6 papers · 1 filter
Computing Witnesses Using the SCAN Algorithm
Fabian Achammer, Stefan Hetzl, Renate A. Schmidt
Second-order quantifier elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are no…
An abstract fixed-point theorem for Horn formula equations
Stefan Hetzl, Johannes Kloibhofer
We consider a class of formula equations in first-order logic, Horn formula equations, which are defined by a syntactic restriction on the occurrences of predicate variables. Horn…
Computing Witnesses Using the SCAN Algorithm (Extended Preprint)
Fabian Achammer, Stefan Hetzl, Renate A. Schmidt
Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are no…
On the Completeness of Interpolation Algorithms
Stefan Hetzl, Raheleh Jalali
Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The quest…
A Fixed-point Theorem for Horn Formula Equations
Stefan Hetzl, Johannes Kloibhofer
We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula eq…
On the Herbrand content of LK
Bahareh Afshari, Stefan Hetzl, Graham E. Leigh
We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex Sigma-2/Pi-2. The representation takes the form of a typed non-determinis…