5 papers
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…
Subsystems of Open Induction
Stefan Hetzl, Johannes Weiser
We study subsystems of open induction which are strongly connected to methods of automated inductive theorem proving. Specifically, we consider systems obtained from restricting in…
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…