On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs

EasyChair Preprint 8672

Abstract

A GSC-terminating and orthogonal inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. Under certain assumptions, it has been shown that a quantifier- and cut-free cyclic proof of a sequent can be transformed into a rewriting-induction (RI, for short) proof of the corresponding term equation. The RI proof can be transformed back into the cyclic proof, but it is not known how to transform arbitrary RI proofs into cyclic proofs. In this paper, we show that for a quantifier- and logical-connective-free sequent, if there exists an RI proof of the corresponding term equation, then there exists a cyclic proof of some sequent w.r.t. some IDS such that the cyclic proof ensures the validity of the initial sequent. To this end, we show a transformation of the RI proof into such a cyclic proof, a sequent, and an IDS.

Keyphrases: cyclic proof, rewriting induction, sequent calculus, term rewriting

@booklet{EasyChair:8672,
  author    = {Shujun Zhang and Naoki Nishida},
  title     = {On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs},
  howpublished = {EasyChair Preprint 8672},
  year      = {EasyChair, 2022}}