DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.14

Certified Infinite Descent Criteria in Isabelle/HOL

Authors: Jamie Wright, Liron Cohen, Reuben N. S. Rowe, and Andrei Popescu

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. Although these criteria are well studied on paper and implemented in tools, a unified, machine-checked account that relates them to the (abstract) Infinite Descent property has been missing. We present an Isabelle/HOL mechanization of this landscape. We develop a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable Isabelle lemmas for ω-regular reasoning over streams and for Büchi-automata constructions needed by the inclusion proofs.

Cite as

Jamie Wright, Liron Cohen, Reuben N. S. Rowe, and Andrei Popescu. Certified Infinite Descent Criteria in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{wright_et_al:LIPIcs.ITP.2026.14,
  author =	{Wright, Jamie and Cohen, Liron and Rowe, Reuben N. S. and Popescu, Andrei},
  title =	{{Certified Infinite Descent Criteria in Isabelle/HOL}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.14},
  URN =		{urn:nbn:de:0030-drops-269882},
  doi =		{10.4230/LIPIcs.ITP.2026.14},
  annote =	{Keywords: Cyclic Proof, Infinite Descent, Size-Change termination, B\"{u}chi automata}
}

Document

DOI: 10.4230/LIPIcs.CSL.2018.17

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

Authors: Liron Cohen and Reuben N. S. Rowe

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract

Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.

Cite as

Liron Cohen and Reuben N. S. Rowe. Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.CSL.2018.17,
  author =	{Cohen, Liron and Rowe, Reuben N. S.},
  title =	{{Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.17},
  URN =		{urn:nbn:de:0030-drops-96841},
  doi =		{10.4230/LIPIcs.CSL.2018.17},
  annote =	{Keywords: Induction, Transitive Closure, Infinitary Proof Systems, Cyclic Proof Systems, Soundness, Completeness, Standard Semantics, Henkin Semantics}
}

Search Results

Documents authored by Rowe, Reuben N. S.

Certified Infinite Descent Criteria in Isabelle/HOL

Abstract

Cite as

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

Abstract

Cite as

Thanks for your feedback!

Could not send message