Treffer: Unification of Drags and Confluence of Drag Rewriting

Title:
Unification of Drags and Confluence of Drag Rewriting
Authors:
Jouannaud, Jean-Pierre, Orejas, Fernando
Contributors:
Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire de Méthodes Formelles, Université de Paris-Saclay, Université de Paris Saclay, Universitat Politècnica de Catalunya [Barcelona] (UPC)
Publisher Information:
HAL CCSD, 2021.
Publication Year:
2021
Collection:
collection:INRIA-SACLAY
collection:INRIA_TEST
collection:INRIA
collection:LSV-AUTO
collection:GS-COMPUTER-SCIENCE
collection:ENS-CACHAN
collection:CNRS
collection:UNIV-PARIS-SACLAY
collection:FARMAN
collection:ENS-PARIS-SACLAY
collection:ENS-PSACLAY
collection:TESTALAIN1
collection:INRIA2
Subject Terms:
ACM: D.: Software, ACM: F.: Theory of Computation, [INFO.INFO-CL]Computer Science [cs], Computation and Language [cs.CL], [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO]
Original Identifier:
HAL: hal-02562152
Document Type:
E-Ressource preprint<br />Preprints<br />Working Papers
Language:
English
Access URL:
https://hal.inria.fr/hal-02562152
https://hal.inria.fr/hal-02562152v2/document
https://hal.inria.fr/hal-02562152v2/file/Confluence_of_Drag_Rewriting.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.02562152v2
Database:
HAL

Weitere Informationen

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.