# 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

(Recall Substitutions for First-Order Logic, Unification.)

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).