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) 这些定理建立了标准公理系统。