Forward Chaining algorithm for solving HORNSAT. I made this to visualise how the FC algorithm works.

hornfc.py

import random

#horn clause: at most one true

pGoal = 0.1

def randToVar(val, vars):
    val -= vars
    if val >= 0:
        val += 1
    return val

def randHorn(vars, isGoal):
    global pGoal
    size = random.randrange(vars)+1
    vals = random.sample(range(0,vars), size)
    for i in range(0,len(vals)):
        vals[i] = -(vals[i] + 1)
    if not isGoal:
        pos = random.randrange(0,len(vals))
        vals[pos] = -vals[pos]
        
    return vals

def randHornSat(vars, clauses):
    sat = []
    for i in range(0,clauses-1):
        sat.append(randHorn(vars, False))
    sat.append(randHorn(vars, True))
    return sat

def hornStr(cl):
    posVar = -1
    negVars = []
    for v in cl:
        if v > 0:
            posVar = v
        else:
            negVars.append(str(abs(v)))
    
    if len(negVars) > 0:
        negVars = '^'.join(negVars) + ' -> '
    else:
        negVars = ''
        
    if posVar == -1:
        return negVars + 'False'
    return negVars + str(posVar)
    
def printHorn(sat):
    clauses = [] 
    for cl in sat:
        clauses.append(hornStr(cl))
    print('[' + ', '.join(clauses) + ']')


class FC:
    def __init__(self, nVars, sat):
        self.inferred = [False]*(nVars+1)
        self.count = []
        self.queue = []
        self.sat = sat
        for cl in sat:
            nPremises = self.countPremises(cl)
            self.count.append(nPremises)
            if nPremises == 0:
                self.queue.append(self.conclusion(cl))
        
    def conclusion(self, cl):
        for v in cl:
            if v > 0:
                return v
        return False
        
    def countPremises(self, cl):
        n = 0
        for v in cl:
            if v < 0:
                n += 1
        return n

    def display(self):
        pInferred = []
        for i in range(0,len(self.inferred)):
            if self.inferred[i]:
                pInferred.append(str(i))
        print('Inferred: ' + ' '.join(pInferred))
        print('Queue: ' + str(self.queue))
        
    def iterate(self):
        if len(self.queue) == 0:
            return False
    
        p = self.queue[0]
        self.queue = self.queue[1:]
        print('pop ' + str(p))
        if p == False:
            return True
            
        if self.inferred[p]:
            print(str(p) + ' already inferred!')
            self.display()
            return None
            
        self.inferred[p] = True
        for i in range(0,len(self.sat)):
            cl = self.sat[i]
            if -p in cl:
                self.count[i] -= 1
                if self.count[i] == 0:
                    self.queue.append(self.conclusion(cl))
        self.display()
        return None
        

nVars = 5
nClauses = 10
sat = randHornSat(nVars,nClauses)
printHorn(sat)

fc = FC(nVars, sat)
while True:
    s = input()
    result = fc.iterate()
    if result == True or result == False:
        if result:
            print('Conclusion can be deduced')
        else:
            print('Conclusion cannot be deduced')
        break