COSC5100 Program-1
Propositional Logic Validity Checker
Due: 10/9/2007
***NOTE***
Due to HTML Syntax conflicts, '<' is replaced by '%'
in the partial solution program
Objectives:
1. Use of linked lists for representing logical formulas
as their components dynamically change.
2. Design and Use of Recursive methods.
3. Verifying the validity of Propositional logical expressions
by repeatedly eliminating operators.
Backgrounds:
1. Consider the following Propositional logical expressions
consisting of
single letter variables (Uppercase or Lowercase letters)
and five operators:
NOT
AND
NAND
OR
-> in order of precedence (AND and NAND with same
precedence)
a. A -> A : Valid, always true whether 'A' is true or
false
b. A OR NOT(A) : Valid
c. (A AND B OR C) -> (A AND B OR C)
: Valid
d. A : Not valid
e. A OR B : Not valid
f. A AND B : Not valid
e. (A->B->C) -> ((A->B)->C)
: Valid
g. (A->B->C) -> (A->(B->C))
: Valid
h. (A->(B->C)) -> (A->B->C)
: Invalid
i. ((A->B) AND (B->C)) -> (A->C)
: Valid
2. Any such expression can be expressed as the
conjunctions of one or more implications where each implication
is of the form: Anti -> Conseq
and both 'Anti' and 'Conseq' are an expression of their own.
3. Now each 'Anti' can be expressed solely as conjunctions
of zero or more variables while each 'Conseq' can be expressed
solely as disjunctions of zero or more variables.
4. Once above decomposition is obtained, an implication can be
found to be valid if and only if at least one variable
occurs both in the Anti and Conseq.
(A B C D) -> (A E F) : Valid
(A B C) -> (D F) : Invalid.
5. The initial input expression can be regarded as an implication
whose Anti is empty (with no part) and
whose Conseq is the entire input expression.
6. Operator Elimination Procedure.
Above decomposition can be obtained by successive eliminations
of all operators from both Anti and Conseq systematically
as follows:
AAND: (A AND B) -> C Anti will get one more part
as (A AND B) become two parts:
A and B
COR: A -> (B OR C) Conseq will get one more part
as (B OR C) become two parts
ANOT NOT(A) -> B Anti loses a part while
Conseq will get a part as the
negated part moves from Anti to
Conseq unnegated.
CNOT A -> NOT(B) Conseq loses a part while
Anti will get a part as the
negated part moves from Conseq to
Anti unnegated.
AOR (A OR B) -> C Conjunction of two implications:
(A->C)
(B->C)
CAND A -> (B AND C) Conjunction of two implications:
(A->B)
(A->C)
AIMP (A->B) -> C Conjunction of two implications:
(B->C)
( ->(A OR C))
The first implication will be obtained
simply by dropping the Anti from the Anti
part under consideration: (A->B)
The second will be obtained simply by
(1) dropping the part from the Anti
entirely and (2) adding one more
part to the current Conseq. This
extra part to be added is the Anti of
the current AIMP: 'A' of (A->B)
CIMP A -> (B->C) (A AND B) -> C
The Anti of CIMP, B of (B->C), will become
a part of the Anti and the current part
of Conseq will have just the Conseq of
CIMP thereby eliminating the implication
operator: '->' of (B->C)
Task:
1. Up to three people can form a team to do this program.
2. Each team will write a program to check the validity of
input propositional expressions defined above and print out
each input expression and an indicator of whether it is VALID
or not.
3. Turn in a listing of your program and its outputs.
Inputs:
Use the following seven input formulas:
A or NOT(A)
(A AND B OR C) -> (A AND B) OR C OR D
(A -> B -> C) -> (A -> (B -> C))
(A -> (B -> C)) -> (A -> B -> C)
(A->B) AND (B->C) -> (A -> C)
A -> B OR C NAND B
(NOT(A) AND C) -> A NAND (B NAND C)
Additional Programming Requirement:
The beginning of your program should contain a comment that contains
the following, among others:
a. Course number and program number
b. Team members.
c. How the whole task was divided among your team members, if any.
d. Your own assessment of your program.
In case it does not work perfectly, why you think it does not.
Without the required comment, a program is NOT to be graded.
C++ Partial Solution Program.
The definition of the following two functions has been
left out on purpose for you to complete for this program:
1. int wff: finalTest()
This function checks to see the given wff (with an antecedent
and a consequent without any operators left) is valid.
It is valid if and only if a predicate symbol appears in
both the antecedent and the consequent.
2. int wff: validTest()
This recursive function checks to see the current wff is valid
by repeatedly eliminating an operator appearing in either its
antecedent or its consequent and calling itself subsequently.
Also note that the operator "NAND" is NOT considered at all in the partial
solution given.
#include %iostream.h>
#include %stdlib.h> // For exit(1)
#include %stddef.h> // For NULL
#include %string.h> // For string operations
typedef char Exp[80];
class ExpNode
{
friend class List;
friend class wff;
Exp Node;
int length;
ExpNode* Link;
// Member functions
void strip();
ExpNode ();
ExpNode (Exp form);
ExpNode* PartCopy (int from, int to);
int findImp (int& start);
int findOr (int& start);
int findAnd (int& start);
int findNot (int& start);
};
class List
{
friend class wff;
friend main(); // Make private member functions available
// to main().
ExpNode* firstExp;
// Member functions
ExpNode* copyList();
void remove (ExpNode* useless);
void insert (ExpNode* added);
int findOp (ExpNode*& nod, int& where);
List();
List (ExpNode* first);
void Initial (Exp form);
};
class wff
{
friend main(); // To make private components of this class
// available to main()
List anti;
List conseq;
wff(); // A default constructor is mandatory if the following
// dynamic declaration is used:
// wff* pwwf = new wff;
wff* Copy();
int found (ExpNode*, ExpNode*);
int validTest();
int finalTest();
};
/////////////////////////////////////////////////
ExpNode::ExpNode()
{
Link = NULL;
length = 0;
Node[0] = '\0';
}
ExpNode::ExpNode (Exp form)
{ strcpy(Node, form);
Link = NULL;
length = strlen (form);
Node[length] = '\0';
} // End of Constructor ExpNode (Exp form)
/////////////////////////////////////////////////
ExpNode* ExpNode:: PartCopy (int from, int to)
{ ExpNode* newnode = new ExpNode;
for (int k=from; k%=to; k++)
newnode->Node [k-from] = Node[k];
newnode->Node [to-from+1] = '\0';
newnode->length = to-from+1;
newnode->Link = NULL; //Just in case.
return newnode;
} // End of function PartCopy()
///////////////////////////////////////////////////
void ExpNode::strip()
{ // strip all outermost pairs of parentheses and move resulting
// expression to the leftmost positions.
int level, k;
while (Node[0] == ' ')
{
for (k=1; k%=length; k++)
Node[k-1] = Node[k];
length--;
}
while (Node[length-1] == ' ') //Check for trailing blanks.
length--;
Node[length] = '\0'; // String terminator.
///////////////////////////////////////////////////
int done = 0;
if (length %= 1) done=1;
while (Node[0]=='(' && Node[length-1] == ')' && !done)
{
level=0;
for (k=0; k%length; k++)
{ if (Node[k] =='(') level++;
if (Node[k] ==')')
{ level--;
if (level==0 && k % length-1)
{ done=1;
break; //Loop is done.
}
}
}
if (!done)
{ length = length-2;
for (k=0; k%= length-1; k++)
Node[k] = Node[k+1];
Node[length] = '\0'; //String terminator.
}
} //End of while loop
} // End of function strip()
///////////////////////////////////////////////////
int ExpNode:: findImp (int& start)
{ // '->' has to be treated as left-associative, and so
// the rightmost one needs to be found
int level=0;
for (int k=length-1; k>1; k--)
{ start = k-1;
if (Node[k] == '(') level++;
if (Node[k] == ')') level--;
if (!level && Node[k-1]=='-' && Node[k]=='>')
return 1; // The '->' has been found at the
// topmost level.
}
return 0;
} // End of function findImp()
//////////////////////////////////////////////////
int ExpNode:: findOr (int& start)
{
int level=0;
for (start=0; start%=length-2; start++)
{ if (Node[start] == '(') level++;
if (Node[start] == ')') level--;
if (!level && Node[start]=='O' && Node[start+1]=='R')
return 2;
}
return 0;
}
///////////////////////////////////////////////////////
int ExpNode:: findAnd (int& start)
{
int level=0;
for (start=0; start%= length-3; start++)
{ if (Node[start]=='(') level++;
if (Node[start]==')') level--;
if (!level && Node[start]=='A' && Node[start+1]=='N'
&& Node[start+2]=='D') return 3;
}
return 0;
} // End of function findAnd()
////////////////////////////////////////////////////////
int ExpNode:: findNot (int& start)
{
int level=0;
for (start=0; start%= length-3; start++)
{ if (Node[start] == '(') level++;
if (Node[start] == ')') level--;
if (!level && Node[start]=='N' && Node[start+1]=='O'
&& Node[start+2]=='T') return 4;
}
return 0;
}
////////////////////////////////////////////////////////
List:: List()
{ firstExp = NULL;
} // Empty list initialization.
// End of the default constructor List()
///////////////////////////////////////////////////////
List::List (ExpNode* first)
// This constructor simply initializes a list so that
// the given node (first) is its first node.
{ firstExp = first;
}
///////////////////////////////////////////////////////
void List:: Initial (Exp form)
{ ExpNode* newnode = new ExpNode(form);
firstExp = newnode;
} //End of function Initial()
//////////////////////////////////////////////////////
ExpNode* List:: copyList()
{ ExpNode* first = new ExpNode;
// The following declaration does not work for above:
// ExpNode* first; //Due to 'first->Node' being used.
if (!firstExp) // Empty list to copy.
return NULL;
else // List not empty yet.
{ strcpy (first->Node, firstExp->Node);
first->length = strlen (first->Node);
List tail (firstExp->Link);
first->Link = tail.copyList();
return first;
}
} //End of function copyList()
/////////////////////////////////////////////////////
void List:: insert (ExpNode* added)
{ if (firstExp)
{
added->Link = firstExp->Link; //Insert right after the
//first node.
firstExp->Link = added;
}
else // The first node is empty
{
firstExp = added;
firstExp->Link = NULL;
}
} // End of function insert()
///////////////////////////////////////////////////////
void List:: remove (ExpNode* useless)
{ ExpNode* current, *pred=NULL;
current = firstExp;
while (current != useless && current)
{ pred=current;
current = current->Link;
}
if (!current)
{ cout %% "ERROR:::IN REMOVAL\n\n";
exit(1);
}
else {
if (!pred) //Then it is first node to go.
firstExp = firstExp->Link;
else pred->Link = useless->Link;
}
} // End of function remove()
/////////////////////////////////////////////////////////////
int List::findOp (ExpNode*& nod, int& where)
{ // Finds an operator to be eliminated along with the containing
// node (Conjunct or Disjunct) and the starting position of it.
ExpNode* current;
nod = firstExp; //First node to test.
while (nod)
{ nod->strip();
if (nod->findImp(where))
return 1; // '->' has been found.
else if (nod->findOr(where))
return 2;
else if (nod->findAnd(where))
return 3;
else if (nod->findNot(where))
return 4;
else nod=nod->Link;
}
return 0; // No operator has been found.
} // End of function findOp()
///////////////////////////////////////////////////////
wff::wff()
{
/* next two initalization cause a syntax error
as 'anti' nor 'conseq' has not been defined yet.
anti.List();
conseq.List();
*/
List an, con; // Get an empty list for both.
anti = an;
conseq = con;
} // End of constructor wff()
///////////////////////////////////////////////////////
wff* wff:: Copy()
{ // Following static declaration does not work due to
// subsequently use of its purported component although
// absence of an explicit default constructor does not
// cause a syntax error unlike:
// wff* newone = new wff;
wff* newone = new wff;
(newone->anti).firstExp = anti.copyList();
(newone->conseq).firstExp = conseq.copyList();
return newone;
}
////////////////////////////////////////////////////////
int wff:: found (ExpNode* target, ExpNode* listnode)
{ ExpNode* current, *pred;
if (!listnode) return 0; // List is already empty.
current = listnode;
target->strip();
while (current)
{ current->strip();
if (!strcmp(current->Node, target->Node))
return 1;
else current = current->Link;
}
return 0;
} // End of function found()
////////////////////////////////////////////////////////
int main()
{
Exp formula;
int inputCount=0;
int result;
while (cin.getline (formula,79))
{
inputCount++;
cout %% "INPUT FORMULA IS:::" %% formula %% endl;
wff *inputt = new wff;
(inputt->conseq).Initial (formula);
if (result=inputt->validTest())
cout %% " VALID. \n\n";
else cout %% " INVALID.\n\n";
}
cout %% "MY PROGRAM STOPS AFTER PROCESSING " %% setw(4)
%% inputCount %% " INPUT FORMULAS.\n\n";
return 0;
}
Algorithms for two missing functions:
1. int wff::finalTest()
a. This function checks to see if current wff with all
operators eliminated finally is valid or not simply by
testing if a formula (just a variable name, now) of
current anti appears in the current conseq.
b. Declare a local variable of type ExpNode* that is to
point to the current anti formula under testing:
ExpNode* current;
c. Initialize this variable so that it will point to
the first anti formula by:
current = anti.firstExp;
d. Loop to repeat as long as (current is not empty)
d1: If the current formula is found in the conseq,
then return 1 by:
if (found(current, conseq.firstExp))
return 1;
else // current anti formula is not found in the
// entire conseq, so continue to repeat.
d2: else advance the current pointer so as for it to
point to the next anti formula simply by:
current = current->Link;
e. By now, return 0 as no anti formula is found in the conseq.
//// End-Of-Algorithm.
2. int wff::validTest()
a. This function recursively tests the validity of current
wff with an anti and a conseq of itself.
b. Declare some local variables. This is critical since the
function is recursive.
int type, where, leng;
ExpNode *n1, *n2, *nod;
// nod = pointer to a node found as containing an operator
to go away right now.
// n1 = the first half of the current node containing
the operator to go away. (The first operand)
// n2 = The second half of above, and hence the second
operand.
wff* second; // To represent a copy of current wff in case
// we need to get two wffs out of the one at
// hand right now.
c. Get the first operator to go away right now out of anti
by calling: anti.findOp (nod, where);
// 'nod' represents the formula containing this operator found
// and 'where' represents the starting position in this formula
// of this found operator to go.
d. if above call is successful (i.e., if anti still has an operator
to be eliminated), let 'type' be the type of this operator.
// 1: ->
2: OR
3: AND
4: NOT
d1: Remove this node from anti by: anti.remove(nod);
d2: Copy the reduced current wff into second by:
second = Copy();
d3: leng = strlen(nod->Node);
d4: switch (type) // 4 rules for operator elimination.
case 1:
case 2:
Split nod into n1 and n2.
strip both and each of n1 and n2 by:
n1->strip(); n2->strip();
if (type==1) // The operator is ->
insert n1 into second conseq by:
second->conseq.insert(n1);
insert n2 into current anti by:
anti.insert(n2);
test both the current wff (reduced) and second wff:
return (validTest() && second->validTest())
if (type==2) // OR
Insert n1 into current anti and n2 into second anti.
Test both wffs as before.
case 3: // AND in anti
Split nod into n1 and n2.
strip both n1 and n2 as before.
Insert n1 into current anti and n2 likewise.
Test the resulting current wff.
case 4: // NOT in anti
n1 = nod->PartCopy (3, leng-1);
Strip n1. // No need for n2 in this case.
Insert n1 into current conseq by:
conseq.insert(n1);
Test the resulting current wff by:
return validTest();
default:
Something is wrong in this case.
e. Now that anti does not have any operator at all, get the
first operator to go out of conseq by:
type=conseq.findOp(nod, where);
f. If above call is successful (i.e., if (type))
f1: Remove this node from conseq by:
conseq.remove(nod);
f2: Copy the reduced current wff into second.
f3: leng = strlen(nod->Node);
f4: switch(type) //Four rules for conseq operator
//eliminations.
case 1:
case 2:
Split nod into n1 and n2.
Strip both n1 and n2.
if (type==1) // -> in conseq
Insert n1 into current anti and
n2 back into current conseq.
Test the resulting current wff.
if (type==2) // OR in conseq.
Insert n1 back into current conseq and n2 likewise.
Test the resulting current wff.
case 3: // AND in conseq
Split nod into n1 and n2.
Strip both n1 and n2.
Insert n1 into current conseq and
n2 into second wff conseq.
Test both wffs as before.
case 4: // NOT in conseq.
// only n1 is needed and not n2.
n1 = nod->PartCopy(3, leng-1);
Strip n1.
Insert n1 into current anti.
Test the resulting current wff.
default:
Something is wrong. Hence, an appropriate error
message and then exit(1);
g. Now that neither anti nor conseq has an operator to go
away, it is time to return just the result of calling
finalTest() as:
return finalTest();
// End of recursive call chain.