Backward Chaining

Backward Chaining

Backward chaining (or backward reasoning) is an inference method described colloquially as working backward from the goal. It is used in automated theorem prove, inference engines, proof assistants, and other artificial intelligence applications.

How it works

Backward chaining starts with a list of goals (or a hypothesis) and works backwards from the consequent to the antecedent to see if any data supports any of these consequent. An inference engine using backward chaining would search the inference rules until it finds one with a consequent that matches a desired goal. If the antecedent of that rule is known to be true, then it is added to the list of goals (for one's goal to be confirmed one must also provide data that confirms this new rule).

The FOL-BC-Ask is a backward chaining algorithm given bellow. It is called with a list of goals containing an element, the original query, and returns the set of all substitutions satisfying the query.

Algorithm

Function FOL-BC-Ask(KB,goals,@) returns a set of substitutions 

inputs: KB, a knowledge base 

       goals, a list of conjuncts forming a query (@ already applied) 

   @, the current substitution, initially the empty subs. { } 

local variables: answers, a set of substitutions, initially empty { } 

if goals is empty then return {@} 

Q<--  Subst(@,First(goals)) 

for each sentence r in KB where STANDARDIZE-APART(r)=(p1 ^…^pn -->q) and @<--Unify (q,q’) succeeds 

          new_goals<--[p1,..., pn | Rest(goals)] 

          answers<-- FOL-BC-Ask(KB, new_goals, Compose(@’,@)) U answers 

return answers

Implementation

Input instruction:

Program will be given an input file. The first line of the input will be the number of queries (n). Following n lines will be the queries, one per line. For each of them, you have to determine whether it can be proved form the knowledge base or not.

Next line of the input will contain the number of clauses in the knowledge base (m).

Following, there will be m lines each containing a statement in the knowledge base. Each clause is in one of these two formats: 1- p1 ∧ p2 ∧ ... ∧ pn => q
2- facts: which are atomic sentences. Such as p or ~p All the p s and also q are either a literal such as HasPermission(Google,Contacts) or negative of a literal such as ~HasPermission(Google,Contacts).

• Queries will not contain any variables.
• Variables are all single lowercase letters
• All predicates (such as HasPermission) and constants (such as Google) are case-sensitive alphabetical strings that begin with uppercase letters.
• Each predicate has at least one argument. (There is no upper bound for the number of arguments). Same predicate will not appear with different number of arguments.
• See the sample inputs for spacing patterns.
• All of the arguments of the facts are constants. i.e. you can assume that there will be no fact such as HasPermission(x,Contacts) ( which says that everyone has permission to see the contacts!) in the knowledge base.
• You can assume that the input format is exactly as it is described. There are no errors in the given input.

Sample Input:

input.txt

1

B(John,Bob)

13

A(x,y) => B(x,y)

G(x,y) => B(x,y)

C(c,d) => A(c,d)

B(x,y) => G(x,y)

F(y) => G(x,y)

G(x,y) ^ F(y) => H(x,y)

I(z) => F(z)

F(z) => I(z)

C(Jie,Joe)

C(Melissa,Mary)

G(John,Bob)

I(Amy)

F(Bob)

Source Code:

1. #Robiul Hasan Nowshad(Aust37)  
2.   
3. from copy import deepcopy  
4.   
5. kb = {}  
6. list_of_predicates = []  
7. list_of_explored_rules = []  
8.   
9. def fetch_rules(goal):  
10.     global kb  
11.     global list_of_predicates  
12.   
13.     print("fetch_rules for goal:- ", goal)  
14.     list_of_rules = []  
15.     predicate = goal.partition('(')[0]  
16.     print("\t", predicate, kb[predicate]['conc'])  
17.     list_of_rules = list_of_rules + kb[predicate]['conc']  
18.     return list_of_rules  
19.   
20.   
21. def subst(theta, first):  
22.     print("\tsubst: ", theta, first)  
23.     predicate = first.partition('(')[0]  
24.     list = (first.partition('(')[-1].rpartition(')')[0]).split(',')  
25.     print("\t", list)  
26.     for i in range(len(list)):  
27.         if variable(list[i]):  
28.             if list[i] in theta:  
29.                 list[i] = theta[list[i]]  
30.     print("\t", predicate + '(' + ','.join(list) + ')')  
31.     return predicate + '(' + ','.join(list) + ')'  
32.   
33.   
34. def variable(x):  
35.     if not isinstance(x, str):  
36.         return False  
37.     else:  
38.         if x.islower():  
39.             return True  
40.         else:  
41.             return False  
42.   
43.   
44. def compound(x):  
45.     if not isinstance(x, str):  
46.         return False  
47.     else:  
48.         if '(' in x and ')' in x:  
49.             return True  
50.         else:  
51.             return False  
52.   
53.   
54. def list(x):  
55.     if not isinstance(x, str):  
56.         return True  
57.     else:  
58.         return False  
59.   
60.   
61. def unify_var(var, x, theta):  
62.     print("IN unify_var", var, x, theta)  
63.     if var in theta:  
64.         print("var in theta", var, theta)  
65.         return unify(theta[var], x, theta)  
66.     elif x in theta:  
67.         print("x in theta", x, theta)  
68.         return unify(var, theta[x], theta)  
69.     else:  
70.         theta[var] = x  
71.         print("not in theta", theta[var])  
72.         return theta  
73.   
74.   
75. def check_theta(theta):  
76.     for entry in theta:  
77.         if variable(theta[entry]):  
78.             if theta[entry] in theta:  
79.                 print("in check_theta. theta changed")  
80.                 theta[entry] = theta[theta[entry]]  
81.     return theta  
82.   
83.   
84. def unify(x, y, theta):  
85.     print("\tunify", x, y, theta)  
86.     if theta == None:  
87.         print("\tin theta is None")  
88.         return None  
89.     elif x == y:  
90.         print("\tin x=y")  
91.         return check_theta(theta)  
92.     elif variable(x) is True:  
93.         print("\tin variable(x)")  
94.         return unify_var(x, y, theta)  
95.     elif variable(y) is True:  
96.         print("\tin variable(y)")  
97.         return unify_var(y, x, theta)  
98.     elif compound(x) and compound(y):  
99.         print("\tin compound")  
100.         x_args = []  
101.         temp = x.partition('(')[-1].rpartition(')')[0]  
102.         for item in temp.split(','):  
103.             x_args.append(item)  
104.         y_args = []  
105.         temp = y.partition('(')[-1].rpartition(')')[0]  
106.         for item in temp.split(','):  
107.             y_args.append(item)  
108.         x_op = x.partition('(')[0]  
109.         y_op = y.partition('(')[0]  
110.         return unify(x_args, y_args, unify(x_op, y_op, theta))  
111.     elif list(x) and list(y):  
112.         print("\tin list")  
113.         return unify(x[1:], y[1:], unify(x[0], y[0], theta))  
114.     else:  
115.         print("\tin else")  
116.         return None  
117.   
118.   
119. def fol_bc_ask(query, theta):  
120.     global kb  
121.     global list_of_predicates  
122.     global list_of_explored_rules  
123.   
124.     print("Backward Chaining")  
125.     list_of_rules = fetch_rules(query)  
126.     for rule in list_of_rules:  
127.         print("taken RULE", rule)  
128.         list_of_explored_rules = []  
129.         list_of_explored_rules.append(query)  
130.         print("\t",query, "added to list_of_explored_rules")  
131.         lhs = rule.partition('=>')[0]  
132.         rhs = rule.partition('=>')[2]  
133.         print("lhs: ", lhs, " rhs: ", rhs)  
134.         print("theta in rule", theta)  
135.         theta1 = unify(rhs, query, theta)  
136.         if theta1 != None:  
137.             list_of_premises = lhs.split('^')  
138.             print("list_of_premises: ", list_of_premises)  
139.             theta2 = fol_bc_and(theta1, list_of_premises)  
140.             if theta2 != None:  
141.                 return theta2  
142.   
143.     print("None of the rules worked out", query)  
144.     return None  
145.   
146. def fol_bc_and(theta, list_of_premises):  
147.     global kb  
148.     global list_of_predicates  
149.   
150.     print("\tand: ", list_of_premises)  
151.     print("\ttheta: ", theta)  
152.     if theta == None:  
153.         return None  
154.     else:  
155.         if list_of_premises != []:  
156.             temp_list = []  
157.             for each_premise in list_of_premises:  
158.                 temp = subst(theta, each_premise)  
159.                 temp_list.append(temp)  
160.             list_of_premises = temp_list  
161.             first_premise = list_of_premises[0]  
162.             rest_premise = list_of_premises[1:]  
163.             subs = list_of_premises[0]  
164.             if subs != '()':  
165.                 if subs in list_of_explored_rules:  
166.                     print(subs, " already in list_of_explored_rules")  
167.                     return None  
168.                 else:  
169.                     print(subs, " added to list_of_explored_rules")  
170.                     list_of_explored_rules.append(subs)  
171.                 theta = fol_bc_or_sub(subs, {}, rest_premise)  
172.             else:  
173.                 return theta  
174.         return theta    
175.   
176.   
177. def fol_bc_or_sub(query, theta, rest):  
178.     global kb  
179.     global list_of_predicates  
180.   
181.     print("\tOR sub")  
182.     list_of_rules = fetch_rules(query)  
183.     print("\tLIST_OF_RULES", list_of_rules)  
184.     for rule in list_of_rules:  
185.         print("\tRULE", rule)  
186.         lhs = rule.partition('=>')[0]  
187.         rhs = rule.partition('=>')[2]  
188.         print("\n\tlhs: ", lhs, " rhs: ", rhs)  
189.         print("\ntheta in rule", theta)  
190.         theta1 = unify(rhs, query, deepcopy(theta))  
191.         if theta1 != None:  
192.             list_of_premises = lhs.split('^')  
193.             print("\tlist_of_premises: ", list_of_premises)  
194.             theta2 = fol_bc_and(theta1, list_of_premises)  
195.             theta3 = fol_bc_and(theta2, rest)  
196.             if theta3 != None:  
197.                 return theta3  
198.   
199.     print("\tNone of the rules worked out", query)  
200.     return None  
201.   
202.   
203. def add_to_kb(knowledge_base):  
204.     global kb  
205.     global list_of_predicates  
206.   
207.     for sentence in knowledge_base:  
208.         if '=>' not in sentence:  
209.             predicate = sentence.partition('(')[0]  
210.             if predicate not in list_of_predicates:  
211.                 conc = []  
212.                 prem = []  
213.                 conc.append("=>" + sentence)  
214.                 kb[predicate] = {'conc': conc, 'prem': prem}  
215.                 list_of_predicates.append(predicate)  
216.             else:  
217.                 conc = kb[predicate]['conc']  
218.                 prem = kb[predicate]['prem']  
219.                 conc.append("=>" + sentence)  
220.                 kb[predicate] = {'conc': conc, 'prem': prem}  
221.         else:  
222.             clauses = sentence.partition('=>')  
223.             list_of_premises = clauses[0].split('^')  
224.             conclusion = clauses[2]  
225.   
226.             # for conclusion  
227.             predicate = conclusion.partition('(')[0]  
228.             if predicate not in list_of_predicates:  
229.                 conc = []  
230.                 prem = []  
231.                 conc.append(sentence)  
232.                 kb[predicate] = {'conc': conc, 'prem': prem}  
233.                 list_of_predicates.append(predicate)  
234.             else:  
235.                 conc = kb[predicate]['conc']  
236.                 prem = kb[predicate]['prem']  
237.                 conc.append(sentence)  
238.                 kb[predicate] = {'conc': conc, 'prem': prem}  
239.   
240.             # for list_of_premises  
241.             for premise in list_of_premises:  
242.                 predicate = premise.partition('(')[0]  
243.                 if predicate not in list_of_predicates:  
244.                     conc = []  
245.                     prem = []  
246.                     prem.append(sentence)  
247.                     kb[predicate] = {'conc': conc, 'prem': prem}  
248.                     list_of_predicates.append(predicate)  
249.                 else:  
250.                     conc = kb[predicate]['conc']  
251.                     prem = kb[predicate]['prem']  
252.                     prem.append(sentence)  
253.                     kb[predicate] = {'conc': conc, 'prem': prem}  
254.   
255.   
256. def variable(x):  
257.     if not isinstance(x, str):  
258.         return False  
259.     else:  
260.         if x.islower():  
261.             return True  
262.         else:  
263.             return False  
264.   
265. def standardize_variables(knowledge_base):  
266.     label = 0  
267.     result_knowledge_base = []  
268.     for rule in knowledge_base:  
269.         variable_names = {}  
270.         lhs = rule.partition('=>')[0]  
271.         rhs = rule.partition('=>')[2]  
272.         premise = []  
273.         for x in lhs.split('^'):  
274.             premise.append(x)  
275.         result_premise = ""  
276.         for term in premise:  
277.             args = []  
278.             result_term = "" + term.partition('(')[0]  
279.             temp = term.partition('(')[-1].rpartition(')')[0]  
280.             result_item = ""  
281.             for item in temp.split(','):  
282.                 args.append(item)  
283.                 if variable(item):  
284.                     if item not in variable_names:  
285.                         variable_names[item] = "x" + repr(label)  
286.                         item = "x" + repr(label)  
287.                         label = label + 1  
288.                     else:  
289.                         item = variable_names[item]  
290.                 result_item = result_item + item + ","  
291.             result_item = result_item[:len(result_item) - 1]  
292.             result_term = result_term + '(' + result_item + ')' + '^'  
293.             result_premise = result_premise + result_term  
294.         result_premise = result_premise[:len(result_premise) - 1]  
295.   
296.         conclusion = []  
297.         for x in rhs.split('^'):  
298.             conclusion.append(x)  
299.         if conclusion != ['']:  
300.             result_premise = result_premise + "=>"  
301.             for term in conclusion:  
302.                 args = []  
303.                 result_term = "" + term.partition('(')[0]  
304.                 temp = term.partition('(')[-1].rpartition(')')[0]  
305.                 result_item = ""  
306.                 for item in temp.split(','):  
307.                     args.append(item)  
308.                     if variable(item):  
309.                         if item not in variable_names:  
310.                             variable_names[item] = "x" + repr(label)  
311.                             item = "x" + repr(label)  
312.                             label = label + 1  
313.                         else:  
314.                             item = variable_names[item]  
315.                     result_item = result_item + item + ","  
316.                 result_item = result_item[:len(result_item) - 1]  
317.                 result_term = result_term + '(' + result_item + ')' + '^'  
318.                 result_premise = result_premise + result_term  
319.             result_premise = result_premise[:len(result_premise) - 1]  
320.   
321.         result_knowledge_base.append(result_premise)  
322.     return result_knowledge_base  
323.   
324. #Main  
325.   
326. fn="input.txt"  
327. queries = []  
328. knowledge_base = []  
329. f1=open(fn, "r")         
330. input = f1.readlines()   
331. input = [x.strip() for x in input]   
332.   
333. for i in range(1, int(input[0]) + 1):  
334.     queries.append(input[i].replace(" ", ""))   
335. for i in range(int(input[0]) + 2, int(input[int(input[0]) + 1]) + int(input[0]) + 2):  
336.     knowledge_base.append(input[i].replace(" ", ""))  
337. knowledge_base = standardize_variables(knowledge_base)  
338.   
339. kb = {}  
340. list_of_predicates = []  
341. add_to_kb(knowledge_base)  
342.   
343. fileOut = open("output.txt", "w")  
344. for query in queries:  
345.     result = fol_bc_ask(query, {})  
346.     if result != None:  
347.         print("True", result)  
348.         fileOut.write("TRUE" + "\n")  
349.     else:  
350.         print("False", result)  
351.         fileOut.write("FALSE" + "\n")  
352.   
353. fileOut.close()  
354. f1.close  

Output File:

TRUE

Here our output file contain, either our queries which given in input is True or False. 

The step wise process will be shown in command prompt.

Github Link: https://github.com/nowshad7/BackwardChaining
Reference: https://homepage.cs.uri.edu/~cingiser/csc481/chapter_notes/amarant.pdf