|Títol||Implementing Inequality and Nondeterministic Specifications with Bi-rewriting Systems|
|Publication Type||Conference Paper|
|Year of Publication||1992|
|Authors||Levy J, Agustí-Cullell J|
|Conference Name||Lecture Notes in Computer Science|
Rewriting with non-symmetric relations can be considered as a computational model of many specification languages based on non-symmetric relations. For instance, Logics of Inequalities, Ordered Algebras, Rewriting Logic, Order-Sorted Algebras, Subset Logic, Unified Algebras, taxonomies, subtypes, Refinement Calculus, all them use some kind of non-symmetric relation on expressions. We have developed an operational semantics for these inequality specifications named bi-rewriting systems. In this paper we show the applicability of bi-rewriting systems to Unified Algebras and nondeterministic specifications. In the first case, we give a canonical bi-rewriting system implementing the basic theory of these algebras. In the second case, nondeterministic specifications are viewed as inclusion specifications, thus bi-rewriting is a sound, although not always complete deduction method. We show how a specification has to be completed in order to have both soundness and completeness.
- Quant a IIIA