Formal Methods in Software Engineering (Fall 2019)
Assignment 2: Propositional and predicate logic Monday, Oct 7, 2019, 12:30pm (upload proof les in OnQ
Important: Please write very legibly in the pencil & paper parts!
1. (30 points) Formalization, manual proof and counter-examples
The goal of this question is to formalize some informal statements or arguments, and either prove them (formally) or disprove them by nding an appropriate counter-example.
You can use the following table as a rough guide on how to map some English terms to the corresponding logical symbol:
Informal English term
Logical symbol/formula
and
∧
or (inclusive or)
∨
not; it is not the case that
¬
neither p nor q
¬p∧¬q
if p then q; q if p; p only if q; p implies q; whenever p then q; q whenever p
p→q
if and only if; equivalent
p↔q
all; for all; every; each; for each; any; for any
∀
exists; there is; there are; at least one; some; for some
∃
Also, when using predicate logic, beware of implicit universal quantica- tions in informal English. For instance, when somebody says A car has 4 wheels, she, of course, means that every car has 4 wheels.
For each of the following arguments:
• (3 points) Formalize the arguments as sequents φ1, . . . , φn ⊢ ψ, i.e., as a collection of premises φ1, . . . , φn and a conclusion ψ in a logic of your choice, and
1
• (7 points) Either:
Show that the argument is valid (by nding a formal proof of the conclusion ψ of the argument from its premises φ1 . . . φn ), or Find a counter-example, that is, a truth assignment l (or model M, if the argument is formalized in predicate logic), such that all premises of the argument are true in l (or M) and the conclusion is false in l (or M).
Hand in
formal proof if there is a proof, or a counter-example, if the argument is not valid. In either case, make sure you explicitly state whether the argument holds or not. Make sure that your proofs only use the rules on page 36, page 47 and page 48 in the notes.
When formalizing an argument statement, write explicitly what atomic proposition or predicate symbol you are using to represent a concept (e.g., P: it is raining; Q(x): x has the u).
Note that some arguments must be formalized with predicate logic while others can be formalized with propositional logic alone. Choose carefully. Also remember to use abstraction, this is, avoid unnecessary detail (you have to decide what is relevant and what is not when you formalize the statements).
(a) If the initialization is correct and if the loop terminates, then prop- erty P is true in the nal state. P is true in the nal state. Therefore, if the initialization is correct, the loop terminates
(b) If Alice is in Sweden, then Bob is in Turkey. If Bob is not in Turkey, then Alice is not in Sweden. Therefore, Alice is in Sweden if and only if Bob is in Turkey
(c) Every customer who has asked for a refund has not received a refund. Someone has received a refund. Therefore, there exists a customer who has not asked for a refund.
2. (15 points) Machine-assisted proofs
In this question, use the Jape proof assistant to nd proofs for the sequents below. Download, installation, and use instructions for Jape are given on the last page.
(a) E→(F∧G)⊢(E→F)∧(E→G) (b) (E∧F)→G⊢E→(F →G)
(c) (∀x.P(x))∨(∀x.R(x))⊢∀x.(P(x)∨R(x))
2
your formalization of each of the following statements, and its
3. (10 points) Proof or disproof?
For each of the following say whether the sequent holds or not, and if it holds, give a formal proof (you may use Jape), and if it doesn’t, give a counter-example (as a model):
(a) ∀x.(P(x)∨R(x))⊢(∀x.P(x))∨(∀x.R(x)) (b) ∃x.(P(x)∨R(x))⊢(∃x.P(x))∨(∃x.R(x))
Important: If you have used Jape to prove one of these sequents, please indicate that in your answer to this question, so that it can be considered during the marking.
4. (20 points) Semantics of predicate logic
Consider predicate logic formulas over the set of variables V = {x, y, z}, function symbols F = {f} and predicate symbols P = {P,Q} where the symbols f, P and Q have arities 1, 1, and 2 respectively. Suppose that we have a model M = (DM,FM,PM) where the domain is DM = {a,b,c,d}, the functions are FM = {fM} and the predicates are PM = {PM,QM} with fM and PM are dened as follows:
DM a b c d fM b P M true true false false
Furthermore, QM is dened as follows:
b
b
a
M def Q (x,y)=
true, if (x = a ∧ y = b) ∨ (x = b ∧ y = d) ∨ (x = c ∧ y = b) false, otherwise
For each of the formulas φi below, determine whether M |= φi or M ̸|= φi this is, whether it holds in the model. Write down how you came to the conclusion.
(a) φ1 : ∀x.(∃y.Q(y, x) → P (x)) (b) φ2 :∀y.(Q(f(y),y)→Q(y,y))
(c) φ3 : ∀z.(P(z) → P(f(z))) (d) φ4 : ∀x.∃y.(P (x) ↔ Q(x, y))
3
Downloading and installing Jape: Jape is available for Linux, Windows and MacOS. You can download Jape from the Jape web page at http://www.cs. ox.ac.uk/people/bernard.sufrin/personal/jape.org. For 64-bit systems, which the vast majority of students should have, click on the rst link 64 bit Distribution [v8.1.3] … and download the le appropriate for your operating system. You will need a recent version of Java (1.8).
To install (instructions taken from the Jape page):
• For Windows and MacOS: double-click on the downloaded le.
• For Linux (or if double-clicking failed): open a console window, go to the directory where you downloaded it, for example:
cd Downloads
and execute with java -jar:
java -jar InstallLinuxjape.jar
The executable is called Jape and it is in the directory selected during the installation.
Using Jape: The logic to use is found under examples/natural_deduction/I2L.jt
Open this theory by clicking, in the main Jape menu: File -> Open new theory… and then browse and select it.
Some more info on how to use Jape for the assignment can be found on the Jape for CISC422 page. A more comprehensive description of how to use natural deduction in Jape is given in this manual, also found on Jape’s website.
Submitting Jape proofs: Save all your proofs in Jape in a single le called a2.jp. This includes the solution to Question 2, as well as any other proofs belonging to other questions that you conducted in Jape. Submit your proof le a2.jp by upload to OnQ.
Submitting ‘pencil & paper’ work: Please submit your paper work (e.g., for Questions 1 and 4) during class. Important: Make sure that you include your rst and last name, and your student number!
4