Skolem 标准型就是将谓词逻辑公式中的全称量词和存在量词所管辖的变量映射到 Skolem 函数或无参 Skolem 变量(常量),形成的公式。