Skip to main content

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

Cohen, Liron, Rowe, Reuben (2018) Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In: Leibniz International Proceedings in Informatics. Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, CSL 2018. . LIPICS (doi:10.4230/LIPIcs.CSL.2018.16) (KAR id:67460)

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.

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.4230/LIPIcs.CSL.2018.16
Uncontrolled keywords: Induction, Transitive Closure, Infinitary Proof Systems, Cyclic Proof Systems, Soundness, Completeness, Standard Semantics, Henkin Semantics
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Reuben Rowe
Date Deposited: 29 Jun 2018 13:45 UTC
Last Modified: 16 Feb 2021 13:55 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/67460 (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.