項書き換え
論理学では、論理式から連言標準形(CNF)を得る手続きを項書き換え系として表すことができる。その系の規則は以下の通りである:
¬ ¬ A → A {\displaystyle \neg \neg A\to A} (二重否定の消去)
¬ ( A ∧ B ) → ¬ A ∨ ¬ B {\displaystyle \neg (A\land B)\to \neg A\lor \neg B} (ド・モルガンの法則)
¬ ( A ∨ B ) → ¬ A ∧ ¬ B {\displaystyle \neg (A\lor B)\to \neg A\land \neg B}
( A ∧ B ) ∨ C → ( A ∨ C ) ∧ ( B ∨ C ) {\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)} (分配法則)
A ∨ ( B ∧ C ) → ( A ∨ B ) ∧ ( A ∨ C ) {\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C)}
ここで、矢印( → {\displaystyle \to } )は規則の左辺が右辺に書き換え可能であることを示す(つまり「~ならば~」という条件文ではない)。