Exercise Sheets

Exercise Sheet 1

Exercise Problem 1.2

Instruction

  1. I can bake the cake only if I buy the ingredients today.
  2. I can go to the gym only if I finish my homework early.
  3. I cannot both buy the ingredients and finish homework early.

Therefore, either I will not bake the cake or I will not go to the gym.

Solution

Formalise the atoms of the statements from above as follows:

  • : I will bake the cake.
  • : I will buy the ingredients today.
  • : I will go to the gym.
  • : I will finish my homework early.

Next, we formalise the premises themselves:

Then, the conclusion is:

So, in sequent notation, we want to prove:

todo

Exercise Problem 1.3

The gold is not here 5. Box 2 The gold is not here 6. Box 3 The gold is in Box 2 Only one message is true; the other two are false. Which box has the gold?

Three boxes are presented to you. One contains gold, the other two are empty. Each box has imprinted on it a clue as to its contents; the clues are:
4. Box 1

Exercise Problem 1.4

be a propositional formula with propositional variables such that:

  • is not a propositional atom, and
  • is built from propositional atoms using only and
    How many branches does a splitting tree of have? Provide a sufficiently detailed explanation of your answer.

Exercise Problem 1.5

Instruction

Find a formula that is equivalent to the above formula and is shortest in size. Justify your answer.

Exercise Problem 1.6

Instruction

List all subformulas with negative polarity in the formula above.

Exercise Problem 1.7

Instruction

  1. Which atoms are pure in the above formula?
  2. Compute a clausal normal form of the above formula by applying the CNF transformation algorithm with naming and optimisations based on polarities of the subformulas.
  3. Decide the satisfiability of the computed CNF formula by applying the dDPLL method to . If is satisfiable, give an interpretation which satisfies it.

Exercise Problem 1.8

using only the pure atom rule

Find a model of the formula

Exercise Problem 1.9

Instruction

Exercise Problem 1.10

be a set of formulas. Let a formula occurring only positively in . Consider a Boolean variable not occurring in , nor in . Let be the set of formulas obtained from by replacing in by . Show that is satisfiable if and only if so is the set of formulas .