Inequational Deduction as Term Graph Rewriting

Multi-algebras allow to model nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results.We propose a simple inequational deduction system, based on term graphs, for inferring inclusions of derived relations in a multi-algebra, and we show that term graph rewriting provides a sound and complete implementation of it.