Given two arbitrary terms , do the following terms always exist?

• A term such that and
• A term such that and

For each question, determine if such a term always exists, if it sometimes exists, or if it never exists. Provide a convincing argument for your answer:

• if it always exists, then provide a construction for that term depending on .
• if it sometimes exists, provide values for for which the term exists and for which the term does not exist.
• if it never exists, provide a proof that this is the case.

In your solution, you are allowed to use any results, facts or procedures explained in the lecture notes. Explain clearly what your answer for each question is (always, sometimes, or never), followed by your argument. Solutions are only accepted as a PDF file.

Which of the following terms are unifiable?

Consider the following terms, where is a constant symbol, is a function symbol of arity 2, are function symbols of arity 1, and are variables:

Which of the following statements are true?

For and , which of the following substitutions are such that ?

Somebody typed a term on a keyboard where the keys for comma and parentheses are broken and got the following:

fhxgyfxyghxgyfxy

Suppose we know that the function symbols f, g, h have the respective arities 2, 1, and 3. 

For and , which of the following substitutions are such that ?

For which of the following interpretations of the variables and the function symbols and does the equation hold?

The DPLL algorithm constructs a decision tree in order to determine if a given propositional formula is satisfiable. For example consider the decision tree presented in the lecture notes with 6 leaves for the simple formula 

Your task is to construct a decision tree for the following propositional formula by applying the DPLL algorithm:

,

How many leaves the your decision tree have?

Important:

• Always apply Boolean Constraint Propagation (BCP) as soon as possible.

• When a decision is necessary, choose variables in alphabetical order: for example, split on variable a before b, b before c, etc.

What is the result of BCP((s ∨ t ∨ u) ∧ (¬s ∨ v) ∧ (¬v ∨ w) ∧ (¬w ∨ ¬s) ∧ (¬t) ∧ (¬u))? Repeat until fixpoint.

Given the following formula in CNF:

(a ∨ c) ∧ (a ∨ b ∨ d) ∧ (a ∨  ¬b ∨ ¬c) ∧ (¬a ∨ c ∨ ¬d)

Which of the following statements hold?