CS21001 Assignment 1 -Propositional Logic – Representation and Deduction Solved 

Problem Statement:

Input. Propositional Formula (φ) as strings with propositions, negations, connectives and brackets, ‘(’ and ‘)’ Postfix Formula Representation. Propositional Formula (φ) as strings with propositions, negations, con-

nectives in Postfix format (this will made available to you in code as a string for ready-made processing!) Output. You will be asked to write separate functions for the following parts (in the already supplied code):

1. Represent the postfix propositional formula (φ) as a binary tree (τ) data structure, known as expres- sion tree, which contains propositions as leaf nodes and operators {∧, ∨, ¬, →, ↔} as internal nodes (refer to the left expression tree in Figure 1) (Marks : 5)
2. Print the expression tree (using in-order traversal of τ) and generate the formula (φ) (Marks : 2)
3. Given ⊤/⊥ values for all the propositions, find the outcome of the overall Formula (φ) from its

   expression tree (τ) (Marks : 4)

4. Transformation of the formula step-wise (φ 􏰇 φI 􏰇 φN 􏰇 φC/φD) using the expression tree data

   structure (τ 􏰇 τI 􏰇 τN 􏰇 τC/τD) as follows:

   1. (a)  Implication-Free Form (IFF): Formula (φI ) after elimination of → and ↔
      Procedure: Transform τ to τI and then print φI from τI (Marks : 4)
   2. (b)  Negation Normal Form (NNF): Formula (φN ) where ¬ appears only before propositions Procedure: Transform τI to τN and then print φN from τN (Marks : 4)
   3. (c)  Conjunctive Normal Form (CNF): Formula (φC) with conjuction of disjunctive-clauses where

      each disjunctive-clause is a disjunction of literals

      Procedure: Transform τN to τC and then print φC from τC (Marks : 3)

   4. (d)  Disjunctive Normal Form (DNF): Formula (φD) with disjuction of conjuctive-clauses where each

      conjunctive-clause is a conjunction of literals
      Procedure: Transform τN to τD and then print φD from τD (Marks : 3)

5. Given the expression tree (τ), using exhaustive search, check for the following – (Marks : 5) (a) the validity (⊤) or the invalidity of the formula (whether it is a tautology or not), or
   (b) the satisfiability or the unsatisfiability (⊥) of the formula (whether it is a contradiction or not)

Algorithms:

Expression Tree Formation. Let the generated postfix string from the propositional formula (φ) be PS[1..n]. The recursive function ETF, i.e. τ ← ETF(PS[1..n]), is as follows:

• If n = 1 (i.e. PS[1] is a proposition), then τ = CREATENODE(φ);
• If n > 1 and PS[n] = ¬, then τ = CREATENODE(¬); τ 􏰆→ rightChild = ETF(PS[1..(n − 1)]);
• If n>2 andPS[n]=⋊⋉, then
  τ =CREATENODE(⋊⋉);τ 􏰆→leftChild=ETF(PS[1..(k−1)]);τ 􏰆→rightChild=ETF(PS[k..(n−1)]);
• return τ;
  Here, the primary question is – how to find k for the last step? (this will be explained to you!)

1

Printing Expression Tree. The recursive function ETP(τ ) is as follows: • If τ 􏰆→ element is not NULL, then

PRINT􏰈(􏰉; ETP(τ 􏰆→ leftChild); PRINT(τ 􏰆→ element); ETP(τ 􏰆→ rightChild); PRINT􏰈)􏰉; Here, the PRINT subroutine displays the respective charater as output.

Formula Evaluation. The recursive functionEVAL, i.e. {⊤,⊥}←EVAL(τ,v1,v2,…,vn) (assuming n propo- sitions where each proposition pi (1 ≤ i ≤ n) is assigned a value vi ∈ {⊤, ⊥}), is as follows:

• If τ 􏰆→ element is proposition pi , then return (vi = ⊤)? ⊤ : ⊥;
• If τ 􏰆→ element is ¬, then return (EVAL(τ 􏰆→ rightChild) = ⊤)? ⊥ : ⊤;
• If τ 􏰆→ element is ∧, then return EVAL(τ 􏰆→ leftChild) ∧ EVAL(τ 􏰆→ rightChild);
• If τ 􏰆→ element is ∨, then return EVAL(τ 􏰆→ leftChild) ∨ EVAL(τ 􏰆→ rightChild);
• If τ 􏰆→ element is →, then return 􏰈(EVAL(τ 􏰆→ leftChild) = ⊤) and (EVAL(τ 􏰆→ rightChild) = ⊥)􏰉? ⊥ : ⊤;
• Ifτ􏰆→elementis↔,then
  return 􏰈((EVAL(τ 􏰆→ leftChild) = ⊤) and (EVAL(τ 􏰆→ rightChild) = ⊤))

  or ((EVAL(τ 􏰆→ leftChild) = ⊥) and (EVAL(τ 􏰆→ rightChild) = ⊥))􏰉? ⊤ : ⊥; IFF Transformation. The recursive function IFF, i.e. τI ← IFF(τ ), is as follows:

• Ifτ􏰆→elementis¬,then
/ ∗ IFF(¬φ) = ¬IFF(φ) ∗ /

• If τ 􏰆→ element is {∧, ∨}, then
/∗ IFF(φ1∧φ2)=IFF(φ1)∧IFF(φ2) IFF(φ1 ∨ φ2) = IFF(φ1) ∨ IFF(φ2)

∗ /
/ ∗ IFF(φ1 → φ2) = ¬IFF(φ1) ∨ IFF(φ2) ∗ /

• Ifτ􏰆→elementis→,then
• Ifτ􏰆→elementis↔,then

/∗ IFF(φ1↔φ2)=IFF(φ1→φ2)∧IFF(φ2→φ1) ∗/ • return τ;

Here, φI can be obtained (as a string expression) by calling ETP(τI).
NNF Transformation. The recursive function NNF, i.e. τN ← NNF(τI), is as follows:

• If τI 􏰆→ element is ¬, then

  – if (τI 􏰆→ rightChild) 􏰆→ element is ¬, then / ∗ NNF(¬¬φ) = NNF(φ) ∗ /

  – if (τI 􏰆→ rightChild) 􏰆→ element is ∧, then / ∗ NNF(¬(φ1 ∧ φ2)) = ¬NNF(φ1) ∨ ¬NNF(φ2)

  – if (τI 􏰆→ rightChild) 􏰆→ element is ∨, then / ∗ NNF(¬(φ1 ∨ φ2)) = ¬NNF(φ1) ∧ ¬NNF(φ2)

• If τI 􏰆→ element is {∧, ∨}, then
  /∗ NNF(φ1∧φ2)=NNF(φ1)∧NNF(φ2)

  NNF(φ1 ∨ φ2) = NNF(φ1) ∨ NNF(φ2) ∗ /

• return τI;

∗ / ∗ /

Here, φN can be obtained (as a string expression) by calling ETP(τN).
CNF Transformation. The recursive function CNF, i.e. τC ← CNF(τN), is as follows:

• If τN 􏰆→ element is ∧, then
  /∗ CNF(φ1 ∧ φ2) = CNF(φ1) ∧ CNF(φ2) ∗ /
• If τN 􏰆→ element is ∨, then

/* Distribution Law enforcement */

– if (τN 􏰆→ leftChild) 􏰆→ element is ∧, then
/∗ CNF((φ1l∧φ1r)∨φ2)=CNF(φ1l∨φ2)∧CNF(φ1r∨φ2) ∗/

– if (τN 􏰆→ rightChild) 􏰆→ element is ∧, then
/∗ CNF(φ1∨(φ2l∧φ2r))=CNF(φ1∨φ2l)∧CNF(φ1∨φ2r) ∗/

• return τN;
Here, φC can be obtained (as a string expression) by calling ETP(τC).

DNF Transformation. The recursive function DNF, i.e. τD ← DNF(τN), is as follows: 2

p

q

qq

r

• If τN 􏰆→ element is ∨, then
  / ∗ DNF(φ1 ∨ φ2) = DNF(φ1) ∨ DNF(φ2) ∗ /
• If τN 􏰆→ element is ∧, then

/* Distribution Law enforcement */

– if (τN 􏰆→ leftChild) 􏰆→ element is ∨, then
/∗ DNF((φ1l∨φ1r)∧φ2)=DNF(φ1l∧φ2)∨DNF(φ1r∧φ2) ∗/

– if (τN 􏰆→ rightChild) 􏰆→ element is ∨, the
/∗ DNF(φ1∧(φ2l∨φ2r))=DNF(φ1∧φ2l)∨DNF(φ1∧φ2r) ∗/

• returnτN;
Here, φD can be obtained (as a string expression) by calling ETP(τD).

Exhaustive Search for Validity/Satisfibility. The function CHECK(τ ) is as follows:

• For every value tuple {v1,v2,…,vn} corresponding to n propositions {p1,p2,…,pn},

  ifEVAL(τ,v1,v2,…,vn)=⊤, then print “⟨VALID+SATISFIABLE⟩”

• For every value tuple {v′1,v′2,…,v′n} corresponding to n propositions {p1,p2,…,pn},

  ifEVAL(τ,v′1,v′2,…,v′n)=⊥, then print “⟨INVALID+UNSATISFIABLE⟩”

• Otherwise, for any pair of value tuples {v1,v2,…,vn} and {v′1,v′2,…,v′n} corresponding to n propo- sitions {p1,p2,…,pn} such that, EVAL(τ,v1,v2,…,vn) = ⊤ and EVAL(τ,v′1,v′2,…,v′n) = ⊥, then print “⟨SATISFIABLE+INVALID⟩”, for {v1,v2,…,vn} and {v′1,v′2,…,v′n}, respectively

  Example:

  Input Propositional Formula. φ = (¬p ∧ q) → (p ∧ (r → q))

  Postfix Formula Representation. p ¬ q ∧ p r q → ∧ → (YOUR INPUT STRING)

  Expression Tree Formation. Depending on the recursive call, two types of parse tree (τ) can be formed. Figure 1 shows the representation of such expression trees.

q

p

r

Formula

CNF

pqp

pp OR

qprq

q

Figure 1: Expression Tree Structure for Original Formula and the Corresponding CNF

FormulaEvaluation. {p=⊥,q=⊤,r=⊤} ⇒ φ=⊥ ; {p=⊥,q=⊥,r=⊥} ⇒ φ=⊤ Formula Transformations. The path through which you shall be doing this is as follows:

φ 􏰇 PostFix 􏰇 τ (Print φ) 􏰇 τI (Print φI) 􏰇 τN (Print φN) 􏰇 τC/τD (Print φC/φD)

IFF : φI = IFF(φ) = IFF((¬p∧q)→(p∧(r→q)))=···=¬(¬p∧q)∨(p∧(¬r∨q)) NNF : φN = NNF(φI) = NNF(¬(¬p∧q)∨(p∧(¬r∨q))))=···=(p∨¬q)∨(p∧(¬r∨q))

CNF : φC = CNF(φN) = CNF((p∨¬q)∨(p∧(¬r∨q)))=···=(p∨¬q∨p)∧(p∨¬q∨¬r∨q) DNF : φD = DNF(φN) = DNF((p∨¬q)∨(p∧(¬r∨q)))=···=(p)∨(¬q)∨(p∧¬r)∨(p∧q)

Check for Validity/Satisfibility.

INVALID: {p = ⊥,q = ⊤,r = ×} (× denotes don′t care term) SATISFIABLE : {p = ⊤, q = ×, r = ×} OR {p = ×, q = ⊥, r = ×}

p

3

Sample Execution:

Compile: (C Code) gcc ROLLNO_CT1.c −lm (Please follow the filename convention given!) (C++ Code) g++ ROLLNO_CT1.cpp −lm (Please follow the filename convention given!)

Execution: ./a.out Sample Run:

Enter Propositional Logic Formula: (!p & q) -> (p & (r -> q)) Postfix Representation of Formula: p ! q & p r q -> & ->

++++ PostFix Format of the Propositional Formula ++++ (’-’ used for ’->’ and ’~’ used for ’<->’)
YOUR INPUT STRING: p!q&prq-&-

++++ Expression Tree Generation ++++
Original Formula (from Expression Tree): ( ( ! p & q ) -> ( p & ( r -> q ) ) )

++++ Expression Tree Evaluation ++++
Enter Total Number of Propositions: 3
Enter Proposition [1] (Format: Name <SPACE> Value): p 0 Enter Proposition [2] (Format: Name <SPACE> Value): q 1 Enter Proposition [3] (Format: Name <SPACE> Value): r 1

The Formula is Evaluated as: False

++++ IFF Expression Tree Conversion ++++
Formula in Implication Free Form (IFF from Expression Tree): (!(!p&q)|(p&(!r|q)))

++++ NNF Expression Tree Conversion ++++
Formula in Negation Normal Form (NNF from Expression Tree): ((p|!q)|(p&(!r|q)))

++++ CNF Expression Tree Conversion ++++
Formula in Conjunctive Normal Form (CNF from Expression Tree): (((p|!q)|p)&((p|!q)|(!r|q)))

++++ DNF Expression Tree Conversion ++++
Formula in Disjunctive Normal Form (DNF from Expression Tree): ((p|!q)|((p&!r)|(p&q)))

++++ Exhaustive Search from Expression Tree for Validity / Satisfiability Checking ++++ Enter Number of Propositions: 3
Enter Proposition Names (<SPACE> Separated): p q r
Evaluations of the Formula:

{(p=0)(q=0)(r=0)} : 1 {(p=0)(q=0)(r=1)} : 1 {(p=0)(q=1)(r=0)} : 0 {(p=0)(q=1)(r=1)} : 0 {(p=1)(q=0)(r=0)} : 1 {(p=1)(q=0)(r=1)} : 1 {(p=1)(q=1)(r=0)} : 1 {(p=1)(q=1)(r=1)} : 1

The Given Formula is: < INVALID + SATISFIABLE >

Submit a single C/C++ source file following proper naming convention [ ROLLNO_CT1.c(.cpp) ]. Do not use any global/static variables. Use of STL is allowed.

4