Computational Thinking (CO2412) Tutorial 4.5: Week 22

4.5.1 Concepts

  1. Recapitulate the following concepts from the lecture: Literal, disjunctive clause, conjunctive normal form (CNF), inference, resolution. Raise anything that might be unclear for discussion during the tutorial.
  2. What does it mean that resolution is complete ("a complete calculus," as it was said in the lecture) with respect to proving the satisfiability (or unsatisfiability) of propositional logic statements?

4.5.2 From logic to graphs

Logic and graphs are closely related topics, because facts about the world - facts to which logical reasoning is applied in practice - are often represented as knowledge graphs. For the purpose of the present scenario, consider the case of an undirected graph with three nodes. The nodes are called A, B, and C, and there are no edges from any node to itself. Therefore, there are three possible edges, between A and B, between A and C, and between B and C.

We introduce atomic statements describing the presence of these edges: Let the atomic statement pAB stand for "there is an edge between A and B," whereas its negative literal ¬pAB stands for "there is no edge between A and B;" the same applies to pAC and pBC.

  1. In human language, how would you paraphrase the meaning of the propositional logic statement SA = ¬pAB ∨ ¬pAC?
  2. As above, for statement SB = (pAB ↔ ¬pBC).
  3. As above, for statement SC = (pAC ↔ pBC).
  4. How many literals are there in this scenario?

4.5.3 Conjunctive normal form

Transform the statements above into CNF. (Except for the statement that is already in CNF.) You will need the semantic equivalence rule (R ↔ S) ≡ (R ∨ ¬S) ∧ (¬R ∨ S).

4.5.4 Consistency

Multiple statements S0, S1, … are consistent if their conjunction S0 ∧ S1 ∧ … is satisfiable. In other words, they are consistent if they have a common model: A valuation that satisfies all the statements. Obversely, they are inconsistent if they entail a contradiction, i.e., if S0, S1, … ⊨ False. Since resolution is a complete calculus for proving the (un)satisfiability of a single propositional logic statement, it can also be used to prove the (in)consistency of multiple statements, which is in fact its main use in practice.

  1. Make sure that you understand the concepts, definitions, and claims above. Raise anything that might be unclear for discussion during the tutorial.
  2. Now use resolution to prove that SA, SB, and SC are consistent.
  3. If multiple statements are consistent, they have a common model. Describe a common model of SA, SB, and SC in terms of the valuation (truth values of the atomic statements).
  4. Draw a graph with the nodes A, B, and C and the appropriate edges that fulfils the constraints expressed by all the three statements SA, SB, and SC.

Reminder: Better late than never - remember to submit your tutorial 4.4 feedback form through Blackboard.