Both the bottom-up and top-down propositional proof procedures of Section 5.3.2 can be extended to Datalog. A proof procedure extended for variables must account for the fact that a free variable in a clause means that all instances of the clause are true. A proof may have to use different instances of the same clause in a single proof.