Assignment 2019/4/19
These two questions are exercises for you to use a mechanical theorem prover to solve problems by reasoning or finding models. The theorem prover you need to use is Z3. The official release is here:
https://github.com/Z3Prover/z3
If you use unix, you can install it using pip:
https://pypi.org/project/z3-solver/#description
Here is a good description of how to install it by Bob Moore of UT Austin:
http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo. php/SMT____Z3-INSTALLATION
Problem 1: The Lady or The Tiger Problem (50 pts)
There are three rooms. Each contains either a lady or a tiger but not both. Furthermore, one room contained a lady and the other two contained tigers. Each of the rooms has a sign, and at most one of the three signs was true. The three signs are:
• Room I: A TIGER IS IN THIS ROOM. • Room II: A LADY IS IN THIS ROOM. • Room III: A TIGER IS IN ROOM II. Which room contains the lady?
Problem 2: The Ranking Problem (50 pts)
Given the following facts:
1. Lisa is not next to Bob in the ranking
2. Jim is ranked immediately ahead of a biology major 3. Bob is ranked immediately ahead of Jim
4. One of the women (Lisa and Mary) is a biology major 5. One of the women is ranked first
What are possible rankings for the four people?
3. Bob is ranked immediately ahead of Jim
4. One of the women (Lisa and Mary) is a biology major 5. One of the women is ranked first
What are possible rankings for the four people?
3 Submission
Please submit your solution on Canvas before the due date. You should submit a zip file named as YourStudentID.zip, which includes:
•
for Problem 1: lady.py, which is a z3 query file for your answer. For example, if your answer is that the lady is in room 2, and you use l2 to denote it, then your z3 query file is to check whether not(l2) is consistent with the KB of this problem. For example, the following python code is a z3 query file to check if q follows from p and p ⊃ q:
————————————————————— from z3 import *
p = Bool(’p’)
q = Bool(’q’)
s = Solver() s.add(Implies(p,q)) s.add(p)
# to prove q, add not(q) to see if it causes a contradiction s.add(not(q))
print(s.check()) —————————————————————
for Problem 2: ranking.py, which is your z3 query file to find a model from which to read out a ranking. For example, the following is a python code to compute a model of p∨q and ¬(p∧q):
————————————————————— from z3 import *
p = Bool(’p’)
q = Bool(’q’)
s = Solver()
s.add(or(p,q))
s.add(not(and(p,q)))
print(s.check())
print(s.model()) —————————————————————
•