在Alt-Ergo中判断实数是否为整数的问题及优化方法咨询

问题描述 #

我想在Alt-Ergo 2.4.3中测试一个实数是否为整数，但没找到floor这类函数，于是尝试用教程里的real_of_int函数实现，代码如下：

function real_of_int(n:int):real = n **. 1
predicate is_int_r(a:real) = exists v:int . a = real_of_int(v)

goal g1: real_of_int(0) = 0.0
goal g2: exists v:int . real_of_int(v) = 0.0
goal g3: is_int_r(0.0)

运行结果：

File "test2.ae", line 4, characters 10-30: Valid (0.0000) (3 steps) (goal g1)
File "test2.ae", line 5, characters 10-45: I don't know (0.0000) (9 steps) (goal g2)
File "test2.ae", line 6, characters 10-23: I don't know (0.0013) (11 steps) (goal g3)

虽然real_of_int(0) = 0.0（g1验证通过），但g2里的存在量词无法找到对应的v=0，导致g3也无法验证。

解决方法 #

方法1：添加反向转换函数与公理约束 #

Alt-Ergo的自动推理对存在量词的处理需要明确的反向推导路径，仅定义real_of_int不足以让它自动关联实数0.0和整数0。可以补充一个int_of_real函数，并添加公理约束两者的转换关系：

function real_of_int(n:int):real = n **. 1
function int_of_real(r:real):int
axiom real_int_roundtrip: forall n:int . int_of_real(real_of_int(n)) = n
axiom int_real_roundtrip: forall n:int . real_of_int(int_of_real(real_of_int(n))) = real_of_int(n)

predicate is_int_r(a:real) = exists v:int . a = real_of_int(v)

goal g1: real_of_int(0) = 0.0
goal g2: exists v:int . real_of_int(v) = 0.0
goal g3: is_int_r(0.0)

添加这些公理后，Alt-Ergo可以通过int_of_real(0.0)推导出对应的整数0，从而验证g2和g3。

方法2：直接用公理定义整数实数的等价性 #

如果不需要显式转换函数，也可以直接用公理明确“实数等于某个整数转换来的实数”的判定规则：

predicate is_int_r(a:real) = exists v:int . a = v **. 1

axiom int_real_eq: forall n:int . (n **. 1) = real_of_int(n)
axiom real_int_zero: 0 **. 1 = 0.0

goal g1: real_of_int(0) = 0.0
goal g2: exists v:int . real_of_int(v) = 0.0
goal g3: is_int_r(0.0)

这里通过real_int_zero直接绑定0的整数和实数形式，结合int_real_eq让推理器能关联两者，进而解决存在量词的实例化问题。

方法3：使用具体实例引导推理 #

对于简单的测试场景，可以直接给存在量词提供实例提示，比如在g2中显式指定v=0：

goal g2: exists v:int . v=0 /\ real_of_int(v) = 0.0

这种方式虽然不够通用，但能快速验证单个案例，适合调试阶段使用。

内容的提问来源于stack exchange，提问作者Nick Battle