Skip to main content
Kent Academic Repository

Infinitary and Cyclic Proof Systems for Transitive Closure Logic

Cohen, Liron and Rowe, Reuben N. S. (2018) Infinitary and Cyclic Proof Systems for Transitive Closure Logic. [Preprint] (doi:10.48550/arXiv.1802.00756) (KAR id:65886)


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.

Item Type: Preprint
DOI/Identification number: 10.48550/arXiv.1802.00756
Refereed: No
Other identifier:
Name of pre-print platform: arXiv
Uncontrolled keywords: Transitive Closure Logic, Infinitary Proof Systems, Infinite Descent, Cyclic Proof, Sequent Calculus, Inductive Reasoning
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Reuben Rowe
Date Deposited: 04 Feb 2018 14:25 UTC
Last Modified: 10 Oct 2023 11:52 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.