CVC5 表示“未知”给定编码为 TPTP 的归纳数据类型，尝试为构造函数找到模型

Question

（编辑：请参阅下面的更短的失败示例！）

下面的TPTP问题是我从精益4到TPTP的翻译产生的。 归纳类型被翻译成一堆类型声明和单射公理，例如自然数。 除非我错过了什么，否则 TPTP 本身不支持归纳数据类型，这是我能想到的最好的编码归纳数据类型。

我试图证明自然数的加法是可交换的。

我对 CVC5 的输入：

thf(ty0, type, nat : $tType).
thf(ty1, type, nat_zero : nat).
thf(ty2, type, nat_succ : (nat > nat)).
% Nat.succ.inj
thf(ax3, axiom, (![N : nat]: (![M : nat]: (((nat_succ @ N) = (nat_succ @ M)) => (N = M))))).

% Nat.add
thf(ty5, type, add : (nat > (nat > nat))).
% add x 0 = 0
thf(ax6, axiom, (![X : nat]: (((add @ X) @ nat_zero) = X))).
% add x (b + 1) = 1 + (add x b)
thf(ax7, axiom, (![X : nat]: (![B : nat]: (((add @ X) @ (nat_succ @ B)) = (nat_succ @ ((add @ X) @ B)))))).

% add n m = add m n
thf(goal, conjecture, (![N : nat]: (![M : nat]: (((add @ N) @ M) = ((add @ M) @ N))))).

然而，CVC5没有找到证明或反驳它，而是放弃了

unknown

。 CVC5 似乎试图实例化构造函数，这不是我想要的，而且 它提供的“模型”实际上违反了单射性。

内射性公理还不够吗？我是否缺少 CVC5 的某些选项？这感觉应该是 CVC5 的小菜一碟。

CVC5的输出：

unknown
(
; cardinality of $$unsorted is 1
; rep: (as @$$unsorted_0 $$unsorted)
; cardinality of nat is 7
; rep: (as @nat_0 nat)
; rep: (as @nat_1 nat)
; rep: (as @nat_2 nat)
; rep: (as @nat_3 nat)
; rep: (as @nat_4 nat)
; rep: (as @nat_5 nat)
; rep: (as @nat_6 nat)
(define-fun nat_zero () nat (as @nat_0 nat))
(define-fun nat_succ ((BOUND_VARIABLE_567 nat)) nat (as @nat_0 nat))
(define-fun add ((BOUND_VARIABLE_571 nat) (BOUND_VARIABLE_573 nat)) nat
  (ite (= (as @nat_1 nat) BOUND_VARIABLE_571)
    (ite (= (as @nat_4 nat) BOUND_VARIABLE_573)
      (as @nat_6 nat)
      (ite (= (as @nat_0 nat) BOUND_VARIABLE_573)
        (as @nat_2 nat)
        (as @nat_0 nat)
      )
    )
    (ite (= (as @nat_0 nat) BOUND_VARIABLE_571)
      (ite (= (as @nat_4 nat) BOUND_VARIABLE_573)
        (as @nat_5 nat)
        (ite (= (as @nat_1 nat) BOUND_VARIABLE_573)
          (as @nat_3 nat)
          (as @nat_0 nat)
        )
      )
      (as @nat_0 nat)
    )
)))

相当于以下精益伪代码：

def nat := {n0, n1, n2, n3, n4, n5, n6}
def nat_zero : nat := n0
def nat_succ : nat -> nat := (fun _x => n0)
def add : nat -> nat -> nat
| n1, n4 => n6
| n1, n0 => n3
| n1, _  => n0
| n0, n4 => n5
| n0, n1 => n0
| _ , _  => n0

更小的例子

下面是CVC5放弃的进一步最小化例子：

thf(ty0, type, tA : $tType).
thf(ty1, type, a : tA).
thf(ty3, type, rel : tA > $o).
thf(ax4, axiom, ![VAR_x : tA]: (rel @ VAR_x)).
thf(goal, conjecture, rel @ a).

输出：

unknown
(
; cardinality of $$unsorted is 1
; rep: (as @$$unsorted_0 $$unsorted)
; cardinality of tA is 1
; rep: (as @tA_0 tA)
(define-fun a () tA (as @tA_0 tA))
(define-fun rel ((BOUND_VARIABLE_346 tA)) Bool false)
)