ギルモアのアルゴリズム
ギルモアのアルゴリズム(英: Gilmore's algorithm)は、エルブランの定理にもとづき一階述語論理式が充足不能(unsatisfiable)かどうかを調べる半アルゴリズム(semi-algorithm)である。ギルモアのアルゴリズムは1960年に発表された。