Matematik, bilişim biliminin bir dalı olan evrensel cebir de iki terimin eşit olduğunu ya da olmadığını ispat etmek için kullanılan bir hesap tekniği.

Örnek: Grup teorisinin aksiyomlarını tekrar edelim:

(X · Y) · Z = X · (Y · Z)

X · e = X

X · X-1 = e

X-1 · X = e

Şimdi "e · X = X" eşitliğin doğru olup olmadığını terimleri (aksiyomları uygulayıp) yeniden yazarak ispatlayabiliriz.

Kanıt:

e · X

= (X · X-1) · X

= X · (X-1 · X)

= X · e

= X

Kaynaklar

Franz Baader, Tobias Nipkow. "Term rewriting and all that". Cambridge University Press.