Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/SLD-Resolution

Selective Linear Definite (SLD) Resolution In this section we will introduce a special form of linear resolution for Horn clauses. We will interpret a clause a program by notationing it in the following form: Definition 27 Let be a set of program clauses. Assume a selection function, which gives for a given goal one of its subgoals . Further assume a goal and a selection function which selects . Let be a variant of a clause in , such that and have no variable in common. If is most general unifier of and , the goal is called SLD-resolvent Definition 28 An SLD-deduction (-refutation)of for a set of program clauses and a goal clause is a linear deduction (refutation) in which only SLD-resolution steps occur and is the start clause. An -computed answer substitution for is , where are the mgUs from a SLD-refutation of with selection function . A substitution for is an answer substitution for . It is a correct answer substitution for , if Theorem 11 Let be a set of program clauses, a goal clause and a selection function. For every correct answer substitution for , there is an -computed answer substitution for and a substitution , such that In the Section on Propositional Logic we already explained propositional tableaux and its variants, like the connection calculus and model elimination. In this section we will give model elimination in the first order case. Note that we need one more inference rule, the reduction rule, in this case Definition 29 A clause (normalform) tableau for a set of clauses is a tableau for , whose nodes are literals from and which is constructed by a (possibly infinite) sequence of applications of the following rules: The tree consisting of root and immediate successors , where is a new variant of a clause from is a tableau for (initialisation rule). Let be a tableau for , a branch of , and an new variant of a clause from , such that the link-condition with mgu is satisfied. If the tree is constructed by extending by the subtrees , then is a tableau for (expansion rule). Let be a tableau for , a branch of , a leaf of , and , such that and have a mgu , than is a tableau for (reduction rule). The following are three possible link conditions: No condition. Weak link condition: There is a literal and , such that and have a mgu Strong link condition: There is a leaf of , and , such that and have a mgu . Analog to the propositional case the different link conditions result in different calculi: The empty condition results in a clause normal form tableau calculus. The weak condition results in a connection calculus. The strong link condition results in a model elimination calculus.