June 2001
Intermediate to advanced
2128 pages
82h 43m
English
We show here a slight extension of the Jouannaud and Kounalis and of Dershowitz [1989] approach. Now, we do not assume any set of free constructors nor any equality predicate. Instead, we assume that the axioms of the specifications are oriented into a finite (ground) convergent rewrite system
Examples 3.1 and 2.7 are easy to complete in order to satisfy this condition.
contains all disequalities s ≠ t for terms s,t such that s t and s is not reducible. ...
Read now
Unlock full access