如何在Z3中使用HORN邏輯證明兩個關係相同

由於Horn Logic擅長處理遞歸定義，因此我在Z3中使用Horn Logic對CSP（進程代數）進行建模檢查。但是，我陷入了一些詭計問題。例如，我有以下代碼：如何在Z3中使用HORN邏輯證明兩個關係相同

(declare-rel A (Int)) 
(declare-rel B (Int)) 

(rule (A 1)) 
(rule (A 2)) 

(rule (B 1)) 
(rule (B 2))

然後，我該如何證明A和B是相等的。這與使用Horn邏輯證明Z3中兩組等價的情況類似。

請問，任何人都可以給我一個線索？非常感謝。

來源

2016-02-13 Kun

有一個支持分層否定的引擎。它僅適用於有限域。使用分層否定，您可以檢查等價。例如：

(declare-rel A ((_ BitVec 8))) 
(declare-rel B ((_ BitVec 8))) 
(declare-rel q()) 

(rule (A #x01)) 
(rule (A #x02)) 

(rule (B #x01)) 
(rule (B #x02)) 

(declare-var x (_ BitVec 8)) 

(rule (=> (and (A x) (not (B x))) q)) 
(rule (=> (and (B x) (not (A x))) q)) 

(query q)

來源

2016-02-17 21:27:05

非常感謝。因爲Horn邏輯不支持數組操作，所以我必須使用關係模擬集合論。最初，如果字母表是a，b和c，我使用（A a true）（A b true）（A c false）來表示包含a和b的集合。但是，當這個領域不確定時，這種方法有時會非常尷尬。我將細化兩個包含由某些規則生成的列表的進程。所以，我需要否定來找出P中是否存在一個不在Q中的列表。似乎BitVector可以檢查兩個有限元素集。最後，分層否定僅支持BitV？ – Kun

如何在Z3中使用HORN邏輯證明兩個關係相同

回答

相關問題