CS157 Problem Set 4

Assigned:	Thursday, November 12
Due:	Thursday, November 19 at 11:59 pm

Please see the course website for collaboration policy, submission instructions, and regrade policy. You may use Logica with acknowledgement. You may work in groups of up to three. Acknowledge all aid and collaboration.

Ask questions on the course newsgroup. Also check the newsgroup for questions asked by other students and responses from the course staff.

Do not repeat the questions in your submission. Make sure you familiarize yourself with the submÄission system on coursework before the submission deadline.

1. (10 points) Ordered Resolution.

Say whether each of the following strategies is compatible with ordered resolution method, i.e. ordered resolution gets the same conclusions with the restriction as without. (strictly ordered and without using contrapositives.)

If the answer is "not compatible", give an example of a set of premises and a conclusion for which Ordered Resolution and the strategy fail to prove the conclusion.

Identical Clause Elimination
Input Restriction
Pure Literal Elimination
Set of Support Restriction
Tautology Elimination

2. (10 points) Model Elimination. Consider the following premises.

p ∧ q ⇒ s
¬p ∧ ¬q ⇒ t
r ⇐ s ∨ t

Give a formal proof of the following conclusion from these premises using model elimination.

((¬p ∨ ¬q) ⇒ ¬(p ∨ q)) ⇒ r

For the proof, you must use the Model Elimination technique with the set of support strategy and input restriction (Use the goal as the set-of-support). Use the same presentation as the lecture notes. Label each step in the proof with the method used: Reduction, Cancellation, or Dropping.

3. (10 points) Model Elimination Caching. The Astrachan and Stickel method for caching in Model Elimination Theorem Provers is designed to work with Horn clauses only. Show an example of a non-Horn premise set where the method fails (i.e. it is either unsound or incomplete).

4. (10 points) Equality.

Give a sentence that is true in an interpretation if and only if the interpretation has at least three elements in its universe of discourse.

Give a sentence that is true in an interpretation if and only if the interpretation has at most three elements in its universe of discourse.

Describe a recusively enumerable set of sentences which is satisfiable but only in infinite models (i.e. models which have an infinite universe of discourse).

(Extra Credit) Give a single sentence which is satisfiable but only in infinite models.

5. (10 points) Demodulation. For each of the following pairs of clauses, show the result of applying demodulation. If it is not possible, state "not possible".

{p(y, f(a,y))} and {f(x,b) = c}
{q(z, g(d,b)), s(w,y)} and {g(x,y) = x}
{p(x, f(a)), q(y), r(x,y)} and {f(y) = y, s(w)}

6. (10 points) Paramodulation. We want to show that the following is true.

∀x.∀y.∀z.((x+z = y+z) ⇒ (x = y))

We are given the following assertions, and the beginning of the proof in Epilog style. Please complete it in the space allotted, using the equality axiom given and paramodulation. That is, your proof should have at most 5 additional steps, should be in Epilog style, and can make use of paramodulation.

1.	x = x	(Equality Axiom)
2.	x = x + e	(Group Theory Axiom)
3.	e = x + inv(x)	(Group Theory Axiom
4.	x + (y + z) = (x + y) + z	(Group Theory Axiom)
5.	a = b ?	(Negated Goal)
6.	a + c = b + c	(Negated Goal)
7.	a + e = b ?	5,2 { x ← a }
8.	a + (w + inv(w)) = b ?	7,3 { x ← w }
9.	(a + w) + inv(w) = b ?	8,4 { x ← a, y ← w, z ← inv(w) }
10.
11.
12.
13.
14.

7. (10 points) Paramodulation and Set of Support. Paramodulation is defined as replacing at least one occurrence of a term by another term to which it is equal.
For example,

{p(a, a)}
{a = b}
----------------
{p(a, b)} or {p(b, a)} or {p(b, b)}

Now consider a variant that requires all occurrences of a term to be replaced with the term to which it is equal. Give an example where using this variant of paramodulation with set of support is incomplete.

8. (10 points) Induction Schema.

Consider the following instance of the induction schema.

p(0) ∧ ∀x.(p(x) ⇒ p(s(x))) ⇒ ∀x.p(x)

Is this sentence Valid, Continget or Unsatisfiable? Explain why.

9. (10 points) Natural Numbers. The following sentences define Peano Arithmetic.

∀x.∀y.(x+1=y+1 ⇒ x=y)
∀x.(x+1 ≠ 0)
0 + 1 = 1
∀x.(x+0=x)
∀x.∀y.(x + (y+1) = (x+y) + 1 )
∀x.(x * 0 = 0)
∀x.∀y.(x * (y+1) = (x * y) + x)

We also have our linear induction schema.

(φ(0) ∧ ∀x.(φ(x) ⇒ φ(x+1))) ⇒ ∀x. φ(x)

Note that we have filled in the base case (which is 0) and we have "inlined" the successor function by replacing s(x) with x+1.

Using these premises, give a resolution / paramodulation proof that addition is associative.

∀x.∀y.∀z.((x+y)+z = x+(y+z))

10. (10 points) Definability. Suppose we wanted to define the unary relation "two" for the natural numbers, where our language has equality and the functions: s (successor function). This relation is definable by the following formula:

two(x) ⇔ x = s(s(0))

where x is a free variable. This sentence will be true when and only when the variable assignment maps x to 2. Therefore, the formula defines the relation two. Define the relation for each of the following sections.

We consider the natural numbers N as our domain, and we add equality, addition and multiplication to our language. The only object constant is 0. (So, you may not, for example, say x=1.) Note that the successor function is not present. Define the following relations. That is, provide a sentence that is true when and only when the free variables are mapped to a tuple in the relation.

{0}
{1}
{<m,n> | n is the successor of m in N}

Note: We do not have the successor function in our language. Hint: For part 3 use the definition of {1} you gave in part 2.

Now we consider the real numbers R. We modify equality, addition and multiplication to retain their normal meaning but for reals instead of naturals. Again, the only constant is 0. Define the following relations:

{m | m ≥ 0}
{2}

Hint: does it matter that we are in R instead of N?

(Optional) Feedback.

Tell us what you thought about this problem set:

How hard was it overall? Give a number from 1-10, with 1 being way too easy and 10 being way too hard and 5 being just right.
Did you use Logica? Was it useful?
Any other comments?