Lab 7
This lab's problem description is the same as Assignment 4. However, your lab solution is required to use Forward Chaining algorithm for the ASK method.
Here is a pseudo code of the Forward Chaining function for propositional logic and Horn Form knowledge base:
// pre condition: KB is in Horn Format // q is a propositional logic symbol bool FC_Entails (KB, q) { create a queue, agenda, that is initialized to be empty; create a vector of tuples, inferred; create a vector, clauses, to hold Clause objects; for each clause in KB { if the clause is a single symbol p, agenda.enqueue(p); if the clause has the format body => head, create a Clause object C such that { C.body = list of symbols in body; C.head = head; C.count = number of symbols in body; clauses.add(C); } for each new symbol in the clause that's not in vector inferred, inferred.add(symbol, false); } while (!agenda.isEmpty()) { symbol p = agenda.dequeue(); if (p == q) return true; if (inferred[i].first == p && inforred[i].second == false) { inferred[i].second = true; for each clauses[i] such that p is in clauses[i].body { clauses[i].count --; if (clauses[i].count == 0) { if (clauses[i].head == q) return true; else agenda.enqueue(clauses[i].head); } } } } return false; }
A rough and not very efficient Backward Chaining algorithm:
// pre condition: KB is in Horn Format // q is a propositional logic symbol bool BC_Entails (KB, q) { create a vector of tuples, inferred; create a vector, clauses, to hold Clause objects; for each clause in KB { if the clause is a single symbol p, agenda.enqueue(p); if the clause has the format body => head, create a Clause object C such that { C.body = list of symbols in body; C.head = head; C.count = number of symbols in body; clauses.add(C); } for each new symbol in the clause that's not in vector inferred, inferred.add(symbol, false); } return Recursive_BC_Entails(inferred, clauses, Q); } // pass inferred by reference so that you don't prove same symbol more than once bool Recursive_BC_Entails(inferred, clauses, Q) { if (Q is in inferred) return true; bool flag; for each c in clauses { if (c.head == Q) { flag = true; for (each sym in c.body, while flag is true) if (Recursive_BC_Entails(inferred, clauses, sym)) { add sym to inferred; } else { flag = false; break; } } } if (flag == true) { add Q to inferred; return true; } } return false; }