Unification of Drags and Confluence of Drag Rewriting

Jean-Pierre Jouannaud (1, 2) , Fernando Orejas (3)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 LMF - Laboratoire Méthodes Formelles
3 UPC - Universitat Politècnica de Catalunya = Université polytechnique de Catalogne [Barcelona]

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules.

Domaines: Informatique et langage [cs.CL]; Logique en informatique [cs.LO]

Jean-Pierre Jouannaud, Fernando Orejas. Unification of Drags and Confluence of Drag Rewriting. 2021. ⟨hal-02562152v2⟩