1930年にJacques Herbrandが発表

述語論理の充足不能性を、命題論理の充足不能性に還元する