Write a Horn clause inference engine which accepts a filename from the user and reads Horn clauses from that file followed by a query (that is, what you are asking to be proven).

The format of the input file will be one Horn clause per line in PROLOG notation (see section 9.4.2). For example, if the data file contains

B:-A. D:-B,C. A. C. ?D.

then the program will print "TRUE" since it can deduce from the Horn clauses that D is true. Print "FALSE" if you cannot prove the query.

Hint: Use the DPLL_satisfiable function in Fig. 7.17.

To prove D is equivalent to saying the Horn clauses entail (imply) D. Since an implication is only false if the "if" side is true and the "then" side is false, we add "not D" to the list of Horn clauses and call DPLL_satisfiable. If it returns false, that means "not not D" must be true, which is D, which is what we were trying to prove, so output "TRUE." If the query had been E then adding "not E" and calling DPLL_satisfiable would result in true, so output "FALSE."

Hint: In PROLOG notation "not D" can be written :-D. Since the "then" side can always be or'ed with false, this is equivalent to D --> false which is equivalent to "not D." Another way of thinking about it is that the "then" side of a Horn clause is false or'ed with whatever terms are there (in this case none).

Name your program hw2pr3.cpp etc.

function DPLL-SATISFIABLE?(s) returns true or false inputs: s, a sentence in propositional logic clauses the set of clauses in the CNF representation of s symbols a list of the proposition symbols in s return DPLL(clauses, symbols, [) function DPLL(clauses, symbols, model) returns true or false if every clause in clauses is true in model then return true if some clause in clauses is false in model then return false P, value FIND-PURE-SYMBOL( symbols, clauses, model) if P is non-null then return DPLL(clauses, symbols P, model U P-value) P, value FIND-UNIT-CLAUSE(clauses, model) if P is non-null then return DPLL(clauses, symbols P, model U P-value) P FIRST(symbols); rest-REST(symbols) return DPLL(clauses, rest, model U {P-true]) or DPLL(clauses, rest, model U {P-false)) Figure7.17 The DPLL algorithm for checking satisfiabilityf a sentence in propositional logic. The ideas behind FIND-PURE-SYMBOL and FIND-UNIT-CLAUSE are described in the text; each returns a symbol (or null) and the truth value to assign to that symbol. Like TT-ENTAILs?, DPLL operates over partial models. function DPLL-SATISFIABLE?(s) returns true or false inputs: s, a sentence in propositional logic clauses the set of clauses in the CNF representation of s symbols a list of the proposition symbols in s return DPLL(clauses, symbols, [) function DPLL(clauses, symbols, model) returns true or false if every clause in clauses is true in model then return true if some clause in clauses is false in model then return false P, value FIND-PURE-SYMBOL( symbols, clauses, model) if P is non-null then return DPLL(clauses, symbols P, model U P-value) P, value FIND-UNIT-CLAUSE(clauses, model) if P is non-null then return DPLL(clauses, symbols P, model U P-value) P FIRST(symbols); rest-REST(symbols) return DPLL(clauses, rest, model U {P-true]) or DPLL(clauses, rest, model U {P-false)) Figure7.17 The DPLL algorithm for checking satisfiabilityf a sentence in propositional logic. The ideas behind FIND-PURE-SYMBOL and FIND-UNIT-CLAUSE are described in the text; each returns a symbol (or null) and the truth value to assign to that symbol. Like TT-ENTAILs?, DPLL operates over partial models