命題論理式を充足可能性が等価な連言標準形に変換する方法であるTseytin変換（Tseytin Transformation）について紹介します．

有限オートマトンによって認識不可能な言語を非正規言語と呼ぶ．ここでは，ある言語が非正規言語となることを示すのによく用いられるポンピング補題について紹介する．