Inequational Deduction as Term Graph Rewriting
Andrea Corradini, Fabio Gadducci, Wolfram Kahl, Barbara König · Electronic Notes in Theoretical Computer Science · 2007
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.