CODEWITHSUNDEEP
c#z3
Dynamite
Dynamite

Reputation: 361

Using axioms for deductions in z3

I am a new user to Z3 and want it to use some axioms and only those axioms to reduce a formula to another equivalent formula in first order logic. Ex: Use only

1.(p or q) and (p or r) <=> p or (r and q)

2.not(p or q) <=> not(p) and not(q)

3.p and p <=> p

to prove

not(p or (q and r)) <=> (not(p)and not(q)) or (not(p)and not(r))

I use the C# API. I guess it has to use uninterpreted function but I have no idea how to do so.

Plzz Help.

Upvotes: 1

Views: 529

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

You are right, the idea is to use uninterpreted functions and sorts. Here is the problem encoded in Z3: http://rise4fun.com/Z3/Vzns

Z3 does not find a proof using the 3 axioms you provided. Actually, the conclusion does not follow from them. However, it can find a proof if we replace the axiom

p and p <=> p

with

not(not(p)) <=> p

Remark: the encoding in the script above uses uninterpreted sort B instead of Bool. Thus, Z3 will also not try a proof by case analysis nor will try to use the fact that Bool contains only two elements.

Remark: it uses = instead of <=>.

In the following example, we use Z3Py to construct a model that satisfies the 3 axioms you provided, but the conjecture does not hold.

http://rise4fun.com/Z3Py/7H7

Upvotes: 1

Related Questions