1

I'm using Horn Logic in Z3 to model check CSP (Process Algebra), because Horn Logic is good at dealing with recursive definitions. But, I was stuck in some trick problems. For example, I have the following code:

(declare-rel A (Int)) (declare-rel B (Int)) (rule (A 1)) (rule (A 2)) (rule (B 1)) (rule (B 2))

Then, how can I prove A and B are equal. This is similar to proving the equivalence of two sets in Z3 using Horn Logic.

Please, anyone can give me a clue? Many thanks.

Improve this question

1 Answer 1

Reset to default
0

There is an engine that supports stratified negation. It works for finite domains only. Using stratified negation you can check equivalence. For example:

(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)
Improve this answer
Sign up to request clarification or add additional context in comments.

1 Comment

Thank you very much. Because Horn logic does not supports Array operations, I have to simulate the set theory using the relations. Initially, I use (A a true) (A b true) (A c false) to represent the set including a and b if the alphabet is a, b and c. But this approach is sometimes very awkward when the domain is uncertain. I'll refine two processes containing some lists which are generated by some rules. So, I need the negation to find out whether one list in P which is not in Q. It seems the BitVector can check two sets with finite elements. Finally, stratified negation supports BitV only?

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.