arXiv subjects

Stefan Hetzl

Publications and source records attributed to Stefan Hetzl.

18 recordsLinked to original sources

arXiv2026

Computing Witnesses Using the SCAN Algorithm

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 not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the saturation-based SCAN algorithm. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding a witness for the second-order quantifiers that results in a logically equivalent first-order formula. In addition, we provide a prototype implementation of the proposed method.

cs.LO↗

arXiv2025

An abstract fixed-point theorem for Horn formula equations

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 formula equations play an important role in many applications in computer science. We state and prove a fixed-point theorem for Horn formula equations in first-order logic with a least fixed-point operator. Our fixed-point theorem is abstract in the sense that it applies to an abstract semantics which generalises standard semantics. We describe several corollaries of this fixed-point theorem in various areas of computational logic, ranging from the logical foundations of program verification to inductive theorem proving.

cs.LO↗

arXiv2025

Subsystems of Open Induction

We study subsystems of open induction which are strongly connected to methods of automated inductive theorem proving. Specifically, we consider systems obtained from restricting induction to atoms, literals, clauses, and dual clauses. We obtain a complete picture of the relationships between these systems in the language of arithmetic and its sublanguages in terms of inclusion and strict inclusion.

math.LO↗

arXiv2025

Computing Witnesses Using the SCAN Algorithm (Extended Preprint)

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 not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification.

cs.LO↗

arXiv2025

On the Completeness of Interpolation Algorithms

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 question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(P)$. We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.

cs.LO↗

arXiv2023

Quantifier-free induction for lists

We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list $\mathit{nil}$ and the operation $\mathit{cons}$, that adds an element to the front of a list. First we show that, for $m \geq 1$, quantifier-free $m$-step induction does not simulate quantifier-free $(m + 1)$-step induction. Secondly, we show that for all $m \geq 1$, quantifier-free $m$-step induction does not prove the right cancellation property of the concatenation operation on lists defined by left-recursion.

math.LO↗

arXiv2022

Induction and Skolemization in saturation theorem proving

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 practically relevant setting we establish a Skolem-free characterization of refutation in saturation-based proof systems with induction. Finally, we use this characterization to obtain unprovability results for a concrete saturation-based induction prover.

math.LO↗

arXiv2022

Unprovability results for clause set cycles

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 discerning the underlying logical features of clause set cycles, we are able to characterize clause set cycles by a logical theory. We make use of this characterization to provide practically relevant unprovability results for clause set cycles that exploit different logical features.

cs.LO↗

arXiv2021

A Fixed-point Theorem for Horn Formula Equations

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 equations. We state and prove a fixed-point theorem for Horn formula equations which is based on expressing the fixed-point computation of a minimal model of a set of Horn clauses on the object level as a formula in first-order logic with a least fixed point operator. We describe several corollaries of this fixed-point theorem, in particular concerning the logical foundations of program verification, and sketch how to generalise it to incorporate abstract interpretations.

cs.LO↗

arXiv2020

Clause Set Cycles and Induction

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 between clause sets. We first show that the formalism of clause set cycles is contained in the theory of $\exists_1$ induction. Secondly we consider the relation between clause set cycles and the theory of open induction. By providing a finite axiomatization of a theory of triangular numbers with open induction we show that the formalism of clause set cycles is not contained in the theory of open induction. Furthermore we conjecture that open induction and clause set cycles are incomparable. Finally, we transfer these results to a concrete method of automated inductive theorem proving called the n-clause calculus.

cs.LO↗

arXiv2018

Some observations on the logical foundations of inductive theorem proving

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 aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving. This is a corrected version of the paper arXiv:1704.01930v5 published originally on Nov.~16, 2017.

cs.LO↗

arXiv2018

Expansion Trees with Cut

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-order logic by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller's expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas. In this paper we present a new syntactic approach that directly extends Miller's expansion trees by cuts and covers also non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and show that it is weakly normalizing.

math.LO↗

arXiv2017

Functional Conceptual Substratum as a New Cognitive Mechanism for Mathematical Creation

We describe a new cognitive ability, i.e., functional conceptual substratum, used implicitly in the generation of several mathematical proofs and definitions. Furthermore, we present an initial (first-order) formalization of this mechanism together with its relation to classic notions like primitive positive definability and Diophantiveness. Additionally, we analyze the semantic variability of functional conceptual substratum when small syntactic modifications are done. Finally, we describe mathematically natural inference rules for definitions inspired by functional conceptual substratum and show that they are sound and complete w.r.t. standard calculi.

math.LO↗

arXiv2016

On the Herbrand content of LK

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-deterministic tree grammar of order 2 which generates a finite language of first-order terms that appear in the Herbrand expansions obtained through cut-elimination. In particular, for every Gentzen-style reduction between LK-proofs we study the induced grammars and classify the cases in which language equality and inclusion hold.

cs.LO↗

arXiv2014

Introducing Quantified Cuts in Logic with Equality

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 the form $\forall x.A$ (for quantifier-free $A$) to a method generating lemmas of the form $\forall x_1\ldots\forall x_n.A$. Moreover, we extend the original method to predicate logic with equality. The new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.

cs.LO↗

arXiv2014

Algorithmic Introduction of Quantified Cuts

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 present in the cut-free proof and then cut-formulas that realize such a compression. Finally, a proof using these cut-formulas is constructed. This method allows an exponential compression of proof length. It can be applied to the output of automated theorem provers, which typically produce analytic proofs. An implementation is available on the web and described in this paper.

cs.LO↗

arXiv2013

Herbrand-Confluence

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 which witnesses they choose for which quantifiers, or in other words: we only consider the Herbrand-disjunction of a cut-free proof. Our main theorem is a confluence result for a natural class of proofs: all (possibly infinitely many) normal forms of the non-erasing reduction lead to the same Herbrand-disjunction.

cs.LO↗

arXiv2013

Expansion Trees with Cut

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-order logic by recording the information which instances have been chosen for which quantifiers, known in the literature as expansion trees. Such a representation is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cut have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas. In this paper we present a new approach that directly extends expansion trees by cuts and covers also non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps. We prove that it is weakly normalizing using methods from the epsilon-calculus.

cs.LO↗