在數學、計算機科學和邏輯學中，重寫涵蓋了用其他術語替換公式中的子項的廣泛方法。這些方法可以通過重寫系統（也被稱為重寫系統、重寫引擎或還原系統）來實現。在其最基本的形式中，它們由一組對象，加上關于如何轉換這些對象的關系組成。重寫可以是非確定性的。一個重寫術語的規則可以以許多不同的方式應用于該術語，或者有多個規則可以適用。因此，重寫系統并不提供將一個術語改為另一個術語的算法，而是提供一組可能的規則應用。然而，當與適當的算法相結合時，重寫系統可以被看作是計算機程序，一些定理證明程序和聲明性編程語言是基于術語重寫的。

在邏輯學中，獲得一個公式的共軛正常形式（CNF）的程序可以作為一個重寫系統來實現。這樣一個系統的例子的規則是。)表示與規則左側相匹配的表達式可以改寫成由右側形成的表達式，而符號則分別表示一個子表達式。在這樣的系統中，每條規則的選擇都是為了使左側與右側等價，因此當左側匹配一個子表達式時，對該子表達式進行從左到右的重寫可以保持邏輯上的一致性和整個表達式的價值。算術術語重寫系統可以用來計算自然數的算術運算。為此，每個自然數必須被編碼為一個術語。最簡單的編碼是Peano公理中使用的編碼，基于常數0（零）和繼任函數S。例如，數字0，1，2和3分別由術語0，S(0)，S(S(0))和S(S(0))表示。

然后，以下術語重寫系統可以用來計算給定自然數的和與積。

在語言學中，短語結構規則，也稱為重寫規則，在一些生成語法系統中使用，作為生成語言的語法正確句子的手段。這種規則通常采用以下形式A→X{displaystyle{rm{ArightarrowX}}，其中A是一個句法的例子。｝其中，A是一個句法類別標簽，如名詞短語或句子，X是這種標簽或語素的序列，表示在生成句子的成分結構時，A可以被X所取代。