Download PDFOpen PDF in browserOn Transforming RewritingInduction Proofs for LogicalConnectiveFree Sequents into Cyclic ProofsEasyChair Preprint no. 867214 pages•Date: August 12, 2022AbstractA GSCterminating and orthogonal inductive definition set (IDS, for short) of firstorder predicate logic can be transformed into a manysorted term rewrite system (TRS, for short) such that a quantifierfree 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 cutfree cyclic proof of a sequent can be transformed into a rewritinginduction (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 logicalconnectivefree 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
