程序代写案例-R3
Mathematical and Logical Foundations of Computer Science
Second Class Test
Question 1 [Linear Algebra]
(a) Consider the following two vectors in R3:
~v =
 12
−1
 ~w =
31
0

(i) Show that ~v and ~w are linearly independent of each other. [2 marks]
(ii) Find a third vector ~u so that {~v, ~w, ~u} form a basis of R3. [2 marks]
(b) The points
P1 =
 31
−3
 P2 =
 10
−2
 P3 =
 20
0

are the corners of a triangle in R3.
(i) Show that the triangle has a right angle, and say at which corner it occurs.
[4 marks]
(ii) The triangle defines a plane E in R3. Give its parametric representation and
its normal form. [4 marks]
(iii) A line L in R3 is given by X =
02
1
 + s ·
03
0
. Compute its point of
intersection with the plane E from the previous item. [4 marks]
(c) Let B = {~v1, ~v2, . . . , ~vn} be a basis for an algebra of vectors V , and let ~w be an
arbitrary vector in V .
(i) When do we say that scalars a1, a2, . . . , an are the coordinates of ~w with respect
to B? [1 mark]
(ii) Prove that the coordinates of ~w with respect to B are uniquely determined.
[3 marks]
Question 2 [SAT & Predicate Logic]
(a) (i) Let p0, p1, q0, q1, r0, r1 be atoms capturing the states of three cells called p, q,
and r , that can each either hold a 0 or a 1: pi captures the fact that cell p
2
35324 LC Mathematical and Logical Foundations of Computer
Science
holds the value i , and similarly for the other atoms. Consider the following
formula:
(p0 ∨ p1) ∧ (q0 ∨ q1) ∧ (r0 ∨ r1) ∧ (¬p0 ∨ ¬p1) ∧ (¬q0 ∨ ¬q1) ∧ (¬r0 ∨ ¬r1)
∧(p0 ∨ q0 ∨ r0) ∧ (p1 ∨ q1) ∧ (p1 ∨ r1) ∧ (q1 ∨ r1)
Using DPLL, prove whether the above formula is satisfiable or not. Detail your
answer. What property of the three cells p, q, and r , is this formula capturing?
[4 marks]
(ii) Given a CNF (Conjunctive Normal Form) that contains a clause composed of
a single literal, can it be proved using Natural Deduction? Justify your answer.
[2 marks]
(b) Consider the following domain and signature:
ˆ Domain: N
ˆ Function symbols: zero (arity 0); succ (arity 1); ∗ (arity 2)
ˆ Predicate symbols: even (arity 1); odd (arity 1); = (arity 2)
We will use infix notation for the binary symbols ∗ and =. Consider the following
formulas that capture properties of the above predicate symbols:
ˆ let S1 be ∀x.(even(x)→ ∃y .x = 2 ∗ y)
ˆ let S2 be ∀x.((∃y .x = succ(2 ∗ y))→ odd(x))
ˆ let S3 be ∀x.∀y .(x = y → succ(x) = succ(y))
where for simplicity we write 0 for zero, 1 for succ(zero), 2 for succ(succ(zero)),
etc.
(i) Provide a constructive Sequent Calculus proof of:
S1, S2, S3 ` ∀x.(even(x)→ odd(succ(x)))
[6 marks]
(ii) Provide a model M such that M ∀x.(even(x)→ odd(succ(x))) [2 marks]
(iii) Provide a model M such that ¬ M ∀x.(even(x)→ odd(succ(x))) [2 marks]
(c) Let p be a predicate symbol of arity 1 and q be a predicate symbol of arity 2. Let F
be the Predicate Logic formula (∀x.(p(x) ∧ ∃y .q(x, y)))→ ∀x.∃y .(p(x) ∧ q(x, y)).
Provide a constructive Natural Deduction proof of F . You are not allowed to make
use of further assumptions so all your hypotheses should be canceled in the final
proof tree. [4 marks]
3

欢迎咨询51作业君
51作业君 51作业君

Email:51zuoyejun

@gmail.com

添加客服微信: ITCSdaixie