CSCI 485 --- Fall 2023

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;
}