Termination, Konfluenz (lokal, global), Normalformen
(literale) Ersetzungsrelation, wohlfundierte monotone Algebra, Polynominterpretation, kritische Paare, Vervollständigung
Größenreduktion, Lovasz-Reduktion, L3
(algebraische) Ersetzung, Simplifikator, Rechnen m. algebr. Zahlen, zulässige Termordnung, S-Polynome, Buchberger-Algorithmus, Euklid als Spezialfall