「形式化」「定式化」「符号化」
「形式化」(formalize, formalization)という言葉の使用例として、自分にとって馴染み深いソフトウェア検証の分野だと、現実世界の形式化されていない問題をまず何らかの形式的体系の上で形式化し、それを必要に応じてより解きやすい別の問題へと符号化(encode)して解くということがしばしば行われる。
例えば、「あるシステムがデッドロックしないことを検証したい」という非形式的な問題があったときに、そのシステムを状態遷移系として、デッドロックしないという性質を時相論理式として形式化することで、元の問題を「ある状態遷移系がある時相論理式を満たすか」という問題に形式化する。 そして、記号モデル検査器(symbolic model checker)はこの問題を充足可能性問題(SAT)等へと符号化して解く。
このような形式化という言葉の用法の起源は、数学における形式主義（数学的な概念や推論を記号や記号処理として捉える考え方）だろう。また、他にも、例えばゲーデルの第二不完全性定理の証明は、（通常非形式的にしか表現しない）第一不完全性定理の証明そのものを算術の体系の内部で形式化することによって証明されたりといった使い方もする。
それに対して、「定式化」(formulate, formulation)という言葉もある。数理最適化分野などではよく使われていて、「形式化」と大体同じ意味だと思うのだけれど、(LPソルバやMIPソルバなどの)特定のソルバが解きやすい問題に落とし込むというような「符号化」的なニュアンスも若干あるように感じる。
また、非形式的なものを形式的体系で表現するのは「形式化」だと思うが、既にある形式的体系の上で表現されているものを別の形式的体系の上で表現するのは「形式化」というよりは「定式化」な気がする。といって、記号モデル検査をSATに符号化することを、「定式化」というかというと、それは言わない気がするし……
特に結論はなくて、オーバーラップしている意味の中で何に重点を置いているかが異なるというだけだと思うのだけれど、言葉は難しい……