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.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Andrea Corradini, Fabio Gadducci, Wolfram Kahl, Barbara König
• Keywords: Algebraic Framework, ENTCS 2007, Simple Inequational Deduction, Term Graph