Unprovability results for clause set cycles

TL;DR

This paper analyzes clause set cycles in automated theorem proving, characterizing their logical features and establishing unprovability results to understand their limitations in inductive reasoning.

Contribution

It introduces a logical characterization of clause set cycles and derives unprovability results based on their logical features, advancing understanding of their capabilities.

Findings

Clause set cycles are characterized by specific logical theories.

Unprovability results depend on the logical features of clause set cycles.

The work provides practical insights into the limitations of clause set cycle methods.

Abstract

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.