7 citations · 23 across the 18 of their papers we have counts for
18 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 obtained from restricting induction to atoms, literals, clauses, and dual clauses. We obtain an almost complete picture of the relationships b…
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…
Quantifier-free induction for lists
Stefan Hetzl, Jannik Vierling
We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list and the operation , that adds an element to t…
Unprovability results for clause set cycles
Stefan Hetzl, Jannik Vierling
The notion of clause set cycle abstracts a family of methods for automated inductive theorem proving based on the detection of cyclic dependencies between clause sets. By discernin…
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…
Induction and Skolemization in saturation theorem proving
Stefan Hetzl, Jannik Vierling
We consider a typical integration of induction in saturation-based theorem provers and investigate the effects of Skolem symbols occurring in the induction formulas. In a practical…
Clause Set Cycles and Induction
Stefan Hetzl, Jannik Vierling
In this article we relate a family of methods for automated inductive theorem proving based on cycle detection in saturation-based provers to well-known theories of induction. To t…
Expansion Trees with Cut
Federico Aschieri, Stefan Hetzl, Daniel Weller
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher…
Functional Conceptual Substratum as a New Cognitive Mechanism for Mathematical Creation
Danny A. J. Gomez-Ramirez, Stefan Hetzl
We describe a new cognitive ability, i.e., functional conceptual substratum, used implicitly in the generation of several mathematical proofs and definitions. Furthermore, we prese…
Some observations on the logical foundations of inductive theorem proving
Stefan Hetzl, Tin Lok Wong
In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of fi…
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…
Introducing Quantified Cuts in Logic with Equality
Stefan Hetzl, Alexander Leitsch, Giselle Reis +2
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of…
Algorithmic Introduction of Quantified Cuts
Stefan Hetzl, Alexander Leitsch, Giselle Reis +1
We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computign a compressed representation of the terms pres…
Herbrand-Confluence
Stefan Hetzl, Lutz Straßburger
We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly…
Expansion Trees with Cut
Stefan Hetzl, Daniel Weller
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view it suggests a compact representation of proofs in classical first- and higher-…