FLOPS 2022 (series) / FLOPS 2022 /
On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs
Wed 11 May 2022 23:35 - 00:00 - Session 7 Chair(s): Hiroshi Unno
An 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. In this paper, to compare rewriting induction (RI, for short) with cyclic proof systems, under certain assumptions, we show that if a sequent has a cut- and quantifier-free cyclic proof, then there exists an RI proof for a term equation of the sequent. To this end, we propose a transformation of a cut- and quantifier-free cyclic proof of the sequent into an RI proof for the corresponding equation.
Wed 11 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
Wed 11 May
Displayed time zone: Osaka, Sapporo, Tokyo change
23:10 - 00:00 | |||
23:10 25mTalk | Asynchronous Unfolding for Fold/Unfold Transformation of Fixpoint Logic Formula FLOPS 2022 Mahmudul Faisal Al Ameen University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan | ||
23:35 25mTalk | On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs FLOPS 2022 |