如何用Z3 Theorem Prover实现Peano算术？代码报错求助

正在学习Z3 Theorem Prover，希望实现Peano算术。此前已在Prolog中完成该实现，现在想要通过可满足性模理论（SMT）求解器来实现。编写的加法实现代码运行时会长时间搜索模型，随后抛出错误：Z3Exception: model is not available.。请指教如何正确实现Peano算术的加法、乘法及小于运算？

用户提供的代码：

from z3 import *

s = Solver()

Nat = Datatype('Nat')
Nat.declare('Z')
Nat.declare('S', ('pred', Nat))
Nat = Nat.create()

Z = Nat.Z
S = Nat.S

P = Function('P', Nat, Nat, Nat, BoolSort())
x, y, z = Consts('x y z', Nat)

s.add(P(Z,Z,Z))
s.add(ForAll([x], P(Z, x, x)))   
s.add(ForAll([x], P(x, Z, x))) 
s.add(ForAll([x,y,z], Implies(P(S(x), y, S(z)), P(x, y, z)))) 

x1 = Const('x1', Nat)
s.add(P(S(Z), S(Z), x1))

if s.check():
  print(s.model())

问题分析 #

你用谓词P表示加法关系，但仅提供了反向推导的公理（从P(S(x),y,S(z))推P(x,y,z)），缺少正向归纳规则（从P(x,y,z)推P(S(x),y,S(z))）。更关键的是，SMT求解器对带全称量词的谓词处理效率极低，容易进入不可判定的搜索空间，导致无法生成模型。改用函数定义运算更符合Z3的能力范围，因为等式理论是Z3擅长的可判定逻辑。

正确实现加法 #

用函数add表示加法，定义基础公理和归纳公理：

• 零加任何数等于该数：add(Z, x) = x
• 后继数加y等于x加y的后继：add(S(x), y) = S(add(x, y))

代码示例：

from z3 import *

# 定义Peano自然数类型
Nat = Datatype('Nat')
Nat.declare('Z')
Nat.declare('S', ('pred', Nat))
Nat = Nat.create()

Z = Nat.Z
S = Nat.S

# 定义加法函数
add = Function('add', Nat, Nat, Nat)
x, y = Consts('x y', Nat)

s = Solver()
# 加法公理
s.add(ForAll([x], add(Z, x) == x))
s.add(ForAll([x, y], add(S(x), y) == S(add(x, y))))

# 测试：1 + 1 = ?
x1 = Const('x1', Nat)
s.add(add(S(Z), S(Z)) == x1)

if s.check() == sat:
    print("加法测试结果：", s.model())

运行后会输出x1 = S(S(Z))，对应Peano算术的2。

扩展实现乘法 #

乘法函数mul的公理：

• 零乘任何数等于零：mul(Z, x) = Z
• 后继数乘y等于y加上x乘y：mul(S(x), y) = add(y, mul(x, y))

在加法代码基础上扩展：

# 定义乘法函数
mul = Function('mul', Nat, Nat, Nat)

# 乘法公理
s.add(ForAll([x], mul(Z, x) == Z))
s.add(ForAll([x, y], mul(S(x), y) == add(y, mul(x, y))))

# 测试：2 * 3 = ?
x2 = Const('x2', Nat)
s.add(mul(S(S(Z)), S(S(S(Z)))) == x2)

if s.check() == sat:
    print("乘法测试结果：", s.model())

输出会是x2 = S(S(S(S(S(S(Z))))))，对应6。

扩展实现小于运算 #

用谓词lt表示小于关系，公理：

• 零小于任何后继数：lt(Z, S(x)) = True
• 任何后继数都不小于零：lt(S(x), Z) = False
• 两个后继数的小于关系等价于其前驱的小于关系：lt(S(x), S(y)) = lt(x, y)

继续扩展代码：

# 定义小于谓词
lt = Function('lt', Nat, Nat, BoolSort())

# 小于运算公理
s.add(ForAll([x], lt(Z, S(x)) == True))
s.add(ForAll([x], lt(S(x), Z) == False))
s.add(ForAll([x, y], lt(S(x), S(y)) == lt(x, y)))

# 测试：1 < 2 和 3 < 2
s.add(lt(S(Z), S(S(Z))) == True)
s.add(lt(S(S(S(Z))), S(S(Z))) == False)

if s.check() == sat:
    print("小于运算测试通过，模型：", s.model())

运行后会验证这两个断言的正确性。

内容的提问来源于stack exchange，提问作者Oleg Dats