Page 57 - 《软件学报》2025年第8期

3480 软件学报 2025 年第 36 卷第 8 期

例如, 在 chain 元规则中 P(x,y) ← Q(x,z),R(z,y), 大写字母 P,Q 和 R 表示存在量化的二阶变量, 而小写字母 x,
y 和 表示全称量化的一阶变量. 每个元规则都与一个阶 (order) 约束相关联, 以确保证明过程的终止. H 表示通过
z
将元替换 Σ = {v 1 /t 1 ,...,v n /t n } 应用到其对应元规则而形成的假设, 其中, 存在量化变量 v i 被替换为项 . MIL 的任务
t i
+ + + − − −
是学习一个假设 H 使得对于 ∀e ∈ E ,B,H ⊨ E 并且对于 ∀e ∈ E ,B,H ⊭ e . 这里 ⊨ 表示蕴涵.

2 问题: 冗余证明
在本节, 我们使用一个具有激励意义的例子“青蛙与荷叶问题”来揭示 MIL 中的冗余证明问题. 青蛙与荷叶问
题的任务描述如下: 有 2n+1 片荷叶和 2n 只青蛙, 其中包括 n 只黄色青蛙和 n 只绿色青蛙. 我们假定每片荷叶最多
只容纳一只青蛙. n 只绿色青蛙蹲在最左边的 n 片荷叶上, 其余 n 只黄色青蛙蹲在最右边的 n 片荷叶上, 中间的荷
叶是空的. 由于荷叶之间的距离限制, 每只青蛙可采用以下两种方式跳跃:
1) 如果青蛙与空荷叶相邻, 它可以直接跳到空荷叶上;
2) 如果青蛙不与空荷叶相邻, 它只能跨过一只青蛙跳到空荷叶上.

目标是找到一种跳跃策略, 以最少的跳跃步数完成在黄蛙和绿蛙之间的位置交换. 例如, 当 n = 2 时, 任务的初
始状态和最终状态如图 1 所示.

初始状态

最终状态

图 1 青蛙与荷叶问题的初始状态和最终状态, 其中 n = 2

我们将绿色青蛙、黄色青蛙和空荷叶分别表示为 1、−1 和 0. 因此, 这个问题的初始状态和最终状态可以表
[−1,−1,0,1,1]. 注意, 青蛙的移动等同于空荷叶的移动. 针对这个任务, 我们设计了 4 个
示为列表 [1,1,0,−1,−1] 和
基本的 2-元谓词 right_one/2、right_two/2、left_one/2 和 left_two/2 (简称为 r1/2、 r2/2、 l1/2 和 l2/2) 来描述空荷
叶的移动. 这些谓词表示空荷叶向其左或右移动了 1 或 2 个位置. 数字 2 表示这些谓词有两个参数 (输入和输出).
例如在图 2 中, 谓词 right_one/2 表示空荷叶移动到了其右侧的第 1 个位置, 这也意味着空荷叶右侧的第 1 只青蛙

跳到了空荷叶上. 因此, 该任务可以描述为一个原子 f ([1,1,0,−1,−1],[−1,−1,0,1,1]). 我们需要基于可用的背景知
P(X,Y) : −Q(X,Z),R(Z,Y). 青蛙与荷
识学习原子 f ([1,1,0,−1,−1],[−1,−1,0,1,1]) 的定义. 此实验使用链式元规则
叶问题的具体输入设置如表 2 所示.

初始状态

right_one/2

图 2 由 2-元谓词 right_one/2 引起的状态变化

表 2 青蛙和荷叶问题的输入设置.

输入 设置
[ ]
实例集 f ([1,1,0,−1,−1],[−1,−1,0,1,1])
元规则集 [P(X,Y) : −Q(X,Z),R(Z,Y)]
背景知识 r1/2 r2/2 l1/2 l2/2
,
,
,

通用元解释器的理论框架如代码 1 所示. 为了生成一个程序, MIL 系统首先尝试通过 (call(Atom)) 将 Atom 作
为目标进行证明. 当证明失败时, MIL 系统尝试将目标与元规则的头部匹配, 检查 Order 约束, 并将元规则中存在
量化的变量绑定到谓词签名中的符号. MIL 系统保存产生的元替换 MetaSub 并尝试证明元规则的体目标. 在证明