Improving basic narrowing techniques and commutation properties

In this paper, we propose a new and complete method based on narrowing for solving equations in equational theories. This method is complete in the sense that it gives all the solutions. It is a combination of basic narrowing, which is not obvious, because their naïve combination is not a complete method. We show that it is more efficient than the existing methods in many cases, and for that establish commutation properties on the narrowing. It provides an algorithm that has been implemented as an extension of the software REVE.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/inria-00075872
Author Rety, Pierre
Maintainer CCSD
Last Updated June 3, 2026, 09:02 (UTC)
Created June 3, 2026, 09:02 (UTC)
Identifier Report N°: RR-0681
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor INRIA Lorraine ; Institut National de Recherche en Informatique et en Automatique (Inria)
creator Rety, Pierre
date 1987-06-03T00:00:00
harvest_object_id 331aac95-317d-4865-99be-a503064fa574
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2023-02-07T00:00:00
set_spec type:REPORT