FLOPS 2022
Tue 10 - Thu 12 May 2022 Online
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 May

Displayed time zone: Osaka, Sapporo, Tokyo change

23:10 - 00:00
Session 7FLOPS 2022
Chair(s): Hiroshi Unno University of Tsukuba; RIKEN AIP
23:10
25m
Talk
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
25m
Talk
On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs
FLOPS 2022
Shujun Zhang Nagoya University, Naoki Nishida Nagoya University