Homework 06 - Due April 9

Problem 1

(Recall Definition of Resolution for FOL.)

Let denote formula

For each of the following formulas, if the formula is valid, use resolution to prove it; if it is invalid, construct at least one Herbrand model for its negation.

a): Formula

b): Formula

c): Formula

d): Formula

e): Formula:

Problem 2

(Recall Sets and Relations.)

We say that a binary relation is a partial order iff it is reflexive, antisymmetric, and transitive. Let be a non-empty set and a binary relation on . Let be the reflexive transitive closure of .

a) Give an example for which is not necessarily a partial order.

b) Define . Show that is a congruence with respect to , that is: is reflexive, symmetric, and transitive and for all ,

c) For each let . Let . Define a new relation, , by

Show that is a partial order on .

Optional: Explain this constructions using terminology of graphs and strongly connected components.

Problem 3

Let be an infinite set of variables. Let be some first-order language. We will consider terms that contain variables from and function symbols from .

Following Problem 2 above, let iff there exists substitution such that where is the standard relation composition.

a) Compute . What is its relationship to ?

b) Compute . Show that relation holds iff where is a relation which is bijection on the set .

Optional: c) Let be a fixed set of syntactic equations. Let be the set of unifiers for and . Show that if is non-empty, then there exists such that for all , we have (that is, is the least element of with respect to defined as in Problem 2).