Lab 2: Proof Engineering with Z3

Overview

In this lab, we'll study how to perform basic theorem proving with Z3 by finishing several exercises. These examples will cover basic logical connectives include implication, disjunction and conjunction. After finishing the examples, you'll do some proofs on your own, these problems will tagged with Exercise. There are some challenging problems which are tagged Challenge, which are optional. Download this code template to start with. For any problems, feel free to ask the TAs for help.

Before starting with this lab, make sure you have finished lab 1 and have Python and Z3 properly installed on your computer.

Hand-in Procedure

When you finished the lab, zip you code files (exclude .venv and other temporary folder) with file name <ID>-lab-2.zip (e.g., SA19225789-lab-2.zip), and submit it to USTC Online Teaching Platform.

Part A: Z3 Basic

In this section, let's start by learning how to do proof development with Z3.

Expression Representation
And /\
Or \/
Not ¬
Implies ->

in which, some key points deserve further explanations:

In this section, we'll learn to use these Expression: And, Or, Not, Implies.

And, Or, Not, Implies

Let's start with an example of And(*args).

Example 1: 
  P, Q, R = Bools('P Q R')
  And(P, Q, R)

Firstly, we need to declare P Q R as Bool type;
then, And(P, Q, R) means proposition : P /\ Q /\ R

We continue to look at our next example of Or(*args):

Example 2: 
  >>> P, Q, R = Bools('P Q R')
  >>> Or(P, Q, R)
  Or(P, Q, R)

Firstly, we need to declare P Q R as Bool type;
then, Or(P, Q, R) means proposition : P \/ Q \/ R

We continue to look at our next example of Not(a):

Example 3: 
  >>> P = Bools('P')
  >>> Not(P)
  Not(P)

Firstly, we need to declare P as Bool type;
then, Not(P) means proposition : ¬P

We continue to look at our next example of Implies(a, b):

Example 4: 
  >>> P, Q = Bools('P Q')
  >>> Implies(P, Q)
  Implies(P, Q)

Firstly, we need to declare P Q as Bool type;
then, Implies(P, Q) means proposition : P -> Q

After learning the usage of these expression, you can try to finish the following exercises.

Exercise 1: Try to define and prove the following propositional logic proposition: $$ P \to ( Q \to P) $$
Exercise 2: Try to define and prove the following propositional logic proposition: $$ (P \to Q) \to ((Q \to R) \to (P \to R)) $$
Exercise 3: Try to define and prove the following propositional logic proposition: $$ (P \wedge ( Q \wedge R )) \to ((P \wedge Q) \wedge R) $$
Exercise 4: Try to define and prove the following propositional logic proposition: $$ (P \vee (Q \vee R)) \to ((P \vee Q) \vee R)$$
Exercise 5: Try to define and prove the following propositional logic proposition: $$ ((P \to R) \wedge (Q \to R)) \to ((P \wedge Q) \to R) $$
Exercise 6: Try to define and prove the following propositional logic proposition: $$ ((P \wedge Q) \to R) \iff (P \to (Q \to R)) $$
Exercise 7: Try to define and prove the following propositional logic proposition: $$ (P \to Q) \to (\neg Q \to \neg P ) $$

Part B: Predicate Logic Proposition

In this section, we'll learn how to prove predicate logic theorems using Z3. In Z3, we have two additional declarations for full quantifiers:

Expression Representation
ForAll ∀x.
Exists ∃x.

in which, some key points deserve further explanations:

In this section, we'll learn to use these Expression: ForAll, Exists.

ForAll, Exists

Let's start with an example of ForAll(vs, body).

Example 5: 
  isort = IntSort()
  bsort = BoolSort()
  
  x = Int('x')
  P = Function('P', isort, bsort)
  ForAll(x, P(x))
  ForAll(x, P(x))

In Z3, sort refers to the type of data or mathematical structure;
Here, IntSort() represents integer sort, BoolSort() represents Boolean sort;
Then an Int variable named 'x' was declared;
Then a function (or predicate) P was declared, with an input of integer type (isort) and an output of Boolean type (bsort)
Finally, we declare the proposition : ForAll(x, P(x)) means proposition : ∀x.P(x)

We continue to look at our next example of Exists(vs, body):

Example 6: 
  isort = IntSort()
  bsort = BoolSort()
  
  x = Int('x')
  P = Function('P', isort, bsort)
  Exists(x, P(x))
  Exists(x, P(x))

Obviously, we declare the proposition : Exists(x, P(x)) means proposition : ∃x.P(x)

After learning the usage of these expression, you can try to finish the following exercises.

Exercise 8: Try to define and prove the following predicate logic proposition: $$\forall x. (\neg p(x) \wedge Q(x)) \to \forall x. (P(x) \to Q(x)) $$
Exercise 9: Try to define and prove the following predicate logic proposition: $$\forall x. (P(x) \wedge Q(x)) \iff (\forall x. P(x) \wedge \forall x.Q(x)) $$
Exercise 10: Try to define and prove the following predicate logic proposition: $$ \exists x. (\neg P(x) \vee Q(x)) \to \exists x. (\neg (P(x) \wedge \neg Q(x))) $$
Exercise 11: Try to define and prove the following predicate logic proposition: $$\exists x. (P(x) \vee Q(x)) \iff (\exists x. P(x) \vee \exists x. Q(x))$$
Exercise 12: Try to define and prove the following predicate logic proposition: $$ \forall x. (P(x) \to \neg Q(x)) \to \neg (\exists x. (P(x) \wedge Q(x)))$$
Exercise 13: Try to define and prove the following predicate logic proposition: $$ \exists x. (P(x) \wedge Q(x)) \wedge \forall x. (P(x) \to R(x)) \to \exists (R(x) \wedge Q(x))$$
Exercise 14: Try to define and prove the following predicate logic proposition: $$ \exists x. \exists y. P(x, y) \to \exists y. \exists x. P(x, y) $$
Exercise 15: Try to define and prove the following predicate logic proposition: $$ P(b) \wedge (\forall x. \forall y. (P(x) \wedge P(y) \to x = y )) \to (\forall x. (P(x) \iff x = b )) $$

Part C: Deduction System

In this section, we need to define some rules to prove the logical theorem.

Challenge: We provide the following two rules : 
    ----------------(odd_1)
          odd 1

          odd n
    ----------------(odd_ss)
        odd n + 2
Please encode these rules using Z3, then prove that integers 9, 25, and 99 are odd numbers.

After finished the lab, don't forget zip you code files with file name <ID>-lab-2.zip (e.g., SA19225789-lab-2.zip), and submit it to USTC Online Teaching Platform.

Happy hacking!