FORMAL LOGIC

Computer Science School of Computing

2.1 Prove by resolution refutation that the formula (pq)r is a logical consequence of the following set of formulas: {(ps)r,qs} For each step in the derivafion, indicate the numbers of parent clauses. 2.2 Use the DPLL algorithm to show that the following set of propositional clauses is satisfiable: {p,pqr,prs,qrs,pqr} Show the set of clauses after each series of propagation. Give the satisfying interpretation determined by this process