Weighted graphs : A tool for logic programming

Unfoldings of oriented graphs generate infinite trees that we generalize by weighting arrows of these graphs. Indexes along a branch are added during unfoldings and the result indexes variables. We study formal properties of these graphs (substitution, equivalence, unification, ...). We use them to solve the halting problem of a recursive head-rewriting rule (as in PROLOG-like languages).