Homework 06 - Due April 9
(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.
(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.
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).