A) 通过为变量分配具体值来解释一阶逻辑公式。
B) 依赖于公理系统的解释。
C) 基于数学归纳法的解释。
D) 软件工程中使用的一种解释。

A) 无需正式证明。
B) 增加证明的复杂性，使其更有说服力。
C) 统一数学证明中使用的符号。
D) 将证明转化为规范形式，以便于分析。

A) 测量数学证明的长度。
B) 计算公式中逻辑连接词的数量。
C) 确定命题的真值。
D) 研究证明数学定理所需的资源。

A) 格哈德-根岑
B) 阿朗佐-丘奇
C) 阿尔弗雷德-塔尔斯基
D) 亨利-庞加莱

A) 形式逻辑中不能使用切割的原则。
B) 所有证明必须消除切割的特性。
C) 切分是有效证明所必需的规则。
D) 每个包含切分的证明都可以转化为无切分证明。

A) 加、减、乘。
B) for, while, do.
C) 如果，那么，否则。
D) 与、或、非。

A) 一种逻辑推理。
B) 证明理论的历史性事件
C) 直观逻辑中证明与计算机程序之间的对应关系。
D) 构建数学证明的规则。

A) 这些定理表明了形式化证明系统的局限性。
B) 这些定理消除了证明复杂性的需要。
C) 这些定理建立了标准公理系统。
D) 这些定理为证明的构建提供了新的技术。