1

关系代数REL051+1.p中的问题读取

  File     : REL051+1 : TPTP v6.1.0. Released v4.0.0.
% Domain   : Relation Algebra
% Problem  : Dense linear ordering

使用 TPTP 语法和 fof 对应的代码是

fof(f01,axiom,(
    ! [A] : o(A,A) )).

fof(f02,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ~ o(B,A) ) )).

fof(f03,axiom,(
    ! [A,B,C] :
      ( ( o(A,B)
        & o(B,C) )
     => o(A,C) ) )).

fof(f04,axiom,(
    ! [A,B] :
      ( ( A != B
        & o(A,B) )
     => ( o(A,f(A,B))
        & o(f(A,B),B) ) ) )).

fof(f05,axiom,(
    ! [A,B] :
      ( f(A,B) != A
      & f(A,B) != B ) )).

fof(f06,axiom,(
    ! [A,B] :
      ( o(A,B)
      | o(B,A) ) )).

正如您在TPTP中看到的，所有 ATP 都无法证明此类问题。

使用以下 SMT-LIB 用 Z3 驳斥了该定理

(declare-sort S)
(declare-fun o (S S) Bool)
(declare-fun f (S S) S)
(assert (forall ((A S)) (o A A) ))
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (not (o B A)))   ) )
(assert (forall ((A S) (B S) (C S)) (implies (and (o A B) (o B C)) 
                                             (o A C))   ) )
(assert (forall ((A S) (B S)) (implies (and (distinct A B) (o A B)) 
                                       (and (o A (f A B)) (o (f A B) B)))   ) )
(declare-fun B () S)
(assert (forall ((A S)) (and (distinct (f A B) A) 
                                   (distinct (f A B) B))    ) )

(assert (not (forall ((A S)) (or (o A B) (o B A)) ) ))

(check-sat)
(get-model)

相应的输出是

    sat
    (model
      ;; universe for S:
      ;;   S!val!0 S!val!3 S!val!1 S!val!2
      ;; -----------
      ;; definitions for universe elements:
      (declare-fun S!val!0 () S)
      (declare-fun S!val!3 () S)
      (declare-fun S!val!1 () S)
      (declare-fun S!val!2 () S)
      ;; cardinality constraint:
      (forall ((x S)) (or (= x S!val!0) (= x S!val!3) (= x S!val!1) (= x S!val!2)))
      ;; -----------
      (define-fun B () S
        S!val!1)
      (define-fun A!0 () S
        S!val!0)
      (define-fun f!47 ((x!1 S) (x!2 S)) S
        (ite (and (= x!1 S!val!2) (= x!2 S!val!1)) S!val!3
          S!val!2))
      (define-fun k!46 ((x!1 S)) S
        (ite (= x!1 S!val!2) S!val!2
        (ite (= x!1 S!val!0) S!val!0
        (ite (= x!1 S!val!3) S!val!3
          S!val!1))))
      (define-fun f ((x!1 S) (x!2 S)) S
        (f!47 (k!46 x!1) (k!46 x!2)))
      (define-fun o!48 ((x!1 S) (x!2 S)) Bool
        (ite (and (= x!1 S!val!1) (= x!2 S!val!1)) true
        (ite (and (= x!1 S!val!0) (= x!2 S!val!0)) true
        (ite (and (= x!1 S!val!2) (= x!2 S!val!2)) true
        (ite (and (= x!1 S!val!3) (= x!2 S!val!3)) true
          false)))))
      (define-fun o ((x!1 S) (x!2 S)) Bool
        (o!48 (k!46 x!1) (k!46 x!2)))
)

请在此处在线运行此示例

我的问题是：这个对 Z3 的反驳是正确的吗？

4

0 回答 0