Search

• < Previous
• 1
• Next >

---

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 normalizing. In this work we take a coarser (and mathematically more realistic) look at cut-free proofs. We analyze&nbsp;[&hellip;]

---

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 this end we introduce the notion of clause set cycles -- a formalism abstracting a certain type of cyclic dependency&nbsp;[&hellip;]

---

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 finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following&nbsp;[&hellip;]

---