Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

Transitive closure logic is a known extension of first-order logic obtained by introducing a

are a priori parametrized by a set of inductive definitions, the addition of the transitive closure

infinitary proof system for transitive closure logic which is an infinite descent-style counterpart

systems for first-order logic with inductive definitions, our infinitary system is complete for the

closure operator allows semantically meaningful complete restrictions to be defined using simple

the basis for an effective system for automating inductive reasoning.