DPLLアルゴリズム
最初、DPLLアルゴリズムはエルブランの定理を用いて一階述語論理式の定理を証明するための方法の一部として、IBM 704上で利用された。それ以前にデービス・パトナムのアルゴリズムにもとづいたプログラムが作成されたが、原子論理式除去規則の実行に多量のメモリが必要だったため、その代わりに分割規則が使用された。分割した節集合は外部記憶装置(磁気テープ)をスタックとして使用し処理を行った。その結果、当時知られていたギルモアのアルゴリズムより高速で複雑な論理式を処理することが可能だった 。
今日でも、DPLLアルゴリズムは命題論理式の充足可能性問題を解くための主要なアルゴリズムの1つとして、多くの定理証明システムで使用されている。