ギルモアのアルゴリズム

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